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.

Install Lea → Join the Discord GitHub

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.

git clone https://github.com/VIDA-NYU/Lea.git
cd Lea
./install.sh --target ui --skip-verify
./start-dev.sh

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 Lea/Misc/SqrtIrrational.lean.

How the proof works

√6 is irrational by norm_num; squaring q = √2 + √3 gives q² = 5 + 2√6, so √6 would be rational — contradiction.

SqrtIrrational.leanstep 5 of 5

import Mathlib
open Real

namespace Lea.Misc

/-- √6 is irrational: 6 is not a square. -/
lemma sqrt_six_irrational :
    Irrational (Real.sqrt 6) := by
  norm_num

/-- The sum √2 + √3 is irrational. -/
theorem irrational_sqrt_two_add_sqrt_three :
    Irrational (Real.sqrt 2 + Real.sqrt 3) := by
  rintro ⟨q, hq⟩
  have h_sq : (q : ℝ) ^ 2 = 5 + 2 * Real.sqrt 6

✓ lean_check: 0 errors 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}
% lea: formalize label=finite_tree_leaves
Every finite tree has at least two leaves.
\end{theorem}

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

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 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

SafeVerifykernel-replay audit — proved vs verified
Lean-LSPthe language server kept warm between edits
Looglefind a lemma by its type signature
sub-agent rolespremise-search and proof-candidate ship
Skills / MCPa 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
description: Looks for a countermodel
tools: [read_file, lean_check, search_mathlib]
max_turns: 12

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 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.

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.

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.

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.