Lea — An agent backbone for mathematician-led formalization.
Skip to content
Formalization that keeps the mathematician in the loop.
Lea is an agent backbone for Lean 4, driving two applications: a standalone web<br>client and an Overleaf extension. You steer how the argument is decomposed, intervene<br>while the proof is being built, and review each claim as it is established.
Install Lea →<br>Join the Discord<br>GitHub
docker<br>local
git clone https://github.com/VIDA-NYU/Lea.git<br>cd Lea/apps/lea-standalone<br>docker compose pull && docker compose upcopy<br>No toolchain to install — Lean and Mathlib are baked into the image. Then open localhost:8001 and paste your API key into Settings.
git clone https://github.com/VIDA-NYU/Lea.git<br>cd Lea<br>./install.sh --target ui --skip-verify<br>./start-dev.shcopy<br>macOS or Linux, Node 22. The script installs uv and elan for you, and adds the Overleaf side.
LeaChat · proof canvas
LLea
✓Done — Proof complete
irrational_sqrt_two_add_sqrt_three is proved and compiles cleanly in<br>Lea/Misc/SqrtIrrational.lean.
How the proof works
√6 is irrational by norm_num; squaring q = √2 + √3 gives<br>q² = 5 + 2√6, so √6 would be rational — contradiction.
SqrtIrrational.leanstep 5 of 5
import Mathlib<br>open Real
namespace Lea.Misc
/-- √6 is irrational: 6 is not a square. -/<br>lemma sqrt_six_irrational :<br>Irrational (Real.sqrt 6) := by<br>norm_num
/-- The sum √2 + √3 is irrational. -/<br>theorem irrational_sqrt_two_add_sqrt_three :<br>Irrational (Real.sqrt 2 + Real.sqrt 3) := by<br>rintro ⟨q, hq⟩<br>have h_sq : (q : ℝ) ^ 2 = 5 + 2 * Real.sqrt 6
✓ lean_check: 0 errors<br>Run SafeVerify
Prove it in the browser
State a theorem in natural language and watch the Lean file take shape beside the transcript. Every step is a version you can walk back through, edit by hand, or hand back.
LeaOverleaf · your LaTeX source
\begin{theorem}\label{thm:leaves}<br>% lea: formalize label=finite_tree_leaves<br>Every finite tree has at least two leaves.<br>\end{theorem}copy
Or straight from Overleaf
Mark a theorem in your paper with a % lea: comment and it gets formalized in place — with uses={…} for dependencies and context={…} for strategy hints.
Set up the extension →
Blueprint · graph view
main_theorem<br>theorem · audit pending
normal_regular_of…<br>lemma · stated
sylow_transitive<br>lemma · ready
stabilizer_index…<br>lemma · audit pending
stabilizer_maximal<br>lemma · audit pending
A decomposition that cannot drift
One blueprint.md, two views. A node is ready when its dependency closure is discharged, and its status is resolved from the latest Lean verdict — never stored as a label someone has to update.
Project · instructions & memory
Burnside Prime Degree Theorem<br>Lea.BurnsidePrimeDegreeTheorem
▤Instructions
Your goal and the rules for Lea. Read on every run — conventions, notation, what counts as done.
◆Memory
Durable facts and learnings. Both you and Lea append: what worked, what failed, dead ends to avoid.
▦Files
Papers and notes Lea can read while it works. PDF · TeX · Markdown · DOCX.
Context that outlives the run
A project fixes a Lean namespace and carries instructions you write plus a memory file you and Lea both append to — what worked, what failed, which dead ends to avoid.
Included · out of the box
Installed and wired on day one
SafeVerify kernel-replay audit — proved vs verified
Lean-LSP the language server kept warm between edits
Loogle find a lemma by its type signature
sub-agent roles premise-search and proof-candidate ship
Skills / MCP a Lean skill and a server config, ready to extend
The Lean tooling is already wired
A kernel-replay audit, a warm Lean language server, Loogle search over Mathlib, specialist sub-agent roles, skills and MCP all ship with Lea. On a general-purpose coding agent, every one of those is something you assemble yourself before you can do any mathematics.
What a fresh install gives you →
Extensibility · a role, in YAML
name: counterexample-hunter<br>description: Looks for a countermodel<br>tools: [read_file, lean_check, search_mathlib]<br>max_turns: 12copy
Extend it without forking it
Skills are markdown, sub-agent roles are YAML, and tools and MCP servers share one registry. Domain knowledge belongs to the mathematician who has it.
Read the source →
Why another formalization system
“81.7% of surveyed mathematics students and researchers preferred full or at least<br>partial human control over the formalization process, and 66.7% wished to retain<br>high-level strategic control even while delegating the mechanical work.”
Collins et al., Characterizing<br>initial human–AI proof formalization workflows (2026)
Autonomy-first systems put the mathematician at the endpoints.<br>You supply a target and inspect a result. Recent harnesses report the consequence<br>themselves: output that type-checks but needs an expert cleanup pass before anyone<br>will maintain it.
General coding agents are domain-neutral by construction.<br>They hand you a loop and expect you to wire in the tools, prompts and scripts....