Introducing Lea: formalization that keeps the mathematician in the loop

Lea is an open-source Lean 4 agent backbone built on one premise — the mathematician steers the decomposition, intervenes mid-proof, and reviews each claim as it is established.