Lea — An agent backbone for mathematician-led formalization.

3 min read Original article ↗

Formalization that keeps the mathematician in the loop.

Lea is an agent backbone for Lean 4, driving two applications: a standalone web client and an Overleaf extension. You steer how the argument is decomposed, intervene while the proof is being built, and review each claim as it is established. 

git clone https://github.com/VIDA-NYU/Lea.git
cd Lea/apps/lea-standalone
docker compose pull && docker compose up

No toolchain to install — Lean and Mathlib are baked into the image. Then open localhost:8001 and paste your API key into Settings.

Why another formalization system

“81.7% of surveyed mathematics students and researchers preferred full or at least partial human control over the formalization process, and 66.7% wished to retain high-level strategic control even while delegating the mechanical work.”

Collins et al., Characterizing initial human–AI proof formalization workflows (2026)

  • Autonomy-first systems put the mathematician at the endpoints. You supply a target and inspect a result. Recent harnesses report the consequence themselves: output that type-checks but needs an expert cleanup pass before anyone will maintain it.
  • General coding agents are domain-neutral by construction. They hand you a loop and expect you to wire in the tools, prompts and scripts. You assemble a system before you do any mathematics.
  • Lea is specialized, and it is a backbone. Lean-specific tools, project memory and blueprints come with it — and the agent is exposed through one API, so mathematician-facing software can be built on top rather than forked from it.

How it works

One run, three moving parts

The prover runs in-process behind a single API. There is no separate prover service to start, and applications react to meaning-level facts, a file changed, a check returned, rather than decoding prover-specific tool output.

LeaChat standalone web client LeaOverleaf Chrome extension + companion One application-neutral API runs · sessions · typed event stream the Lea backbone Controller projects · blueprintssub-agent roles Lean runtime lean_check · MathlibLSP-warm · SafeVerify Run ledger SQLite timelinecontent-addressed act emit history becomes the context for the next action

01

Formalization controller

Works on a project that outlives any single run: a fixed Lean namespace plus instructions, accumulated memory, and a blueprint decomposing the target into interdependent lemmas. It can delegate bounded work to sub-agents with their own budgets and tools.

02

Lean project runtime

Executes each action inside your Lake workspace with a deliberately small tool surface: read, write, edit, lean_check, shell, Mathlib search. Your own tools plug into that surface with a URL and a note on when to use them. Loogle search, for example, takes a few fields in the UI and no code changes.

03

Persistent run ledger

Every run is an ordered stream of typed events, stored as it streams. The live canvas and a page reload read the same bytes, and a client that drops off replays from its last cursor. Statuses are derived from the latest Lean verdict, never stored.