Formal reasoning
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
An agent system that organizes Lean 4 theorem proving around an explicit proof plan, recursive decomposition, and independent checks.
- Year
- 2026
- Status
- Preprint
- Topics
- LLM agents · Formal verification · Lean
Conceptual proof plan: helper statements support a fixed target, and a difficult helper can be split into smaller obligations. The feedback loop revises the plan after a failed check. This diagram illustrates the architecture, not a recorded benchmark trace.
The question
How can an AI agent complete a long formal proof while preserving the mathematical claim it set out to prove?
Central insight
A failed proof attempt can reveal a problem with the plan itself. Recording dependencies explicitly lets the system revise intermediate claims, split difficult steps, and revisit affected proofs while keeping the original target fixed.
Approach
- 01
Anchor the original theorem and organize its prerequisites in a shared proof plan.
- 02
Give each Planning, Lean, or Check agent one focused objective.
- 03
Use compilation and independent checks to decide whether to repair code, split a statement, or revise the plan.
- 04
Require the final proof to preserve the target signature and pass a Lean build and transitive axiom audit.
My contribution
- Built an LLM-agent system that plans, writes, repairs, and verifies Lean 4 proofs through recursive decomposition.
- Developed reusable workflows and CLI/runtime tooling for reliable AI-assisted mathematical formalization.
A closer look
The proof plan as working memory
Long proofs accumulate intermediate lemmas, dependencies, and failed attempts. Keeping all of that inside a growing conversation makes it difficult to remember which claims are established and which assumptions still need justification. MerLean-Prover stores this state in a shared proof plan. Each node has a mathematical statement, a proof sketch, dependencies, and a completion status.
The target carries an anchor: the original Lean declaration, including its parameters, hypotheses, and conclusion. Helpers may change as the search develops, but the completed proof must still establish that original target. When a statement changes, affected downstream statements are invalidated and reconsidered.
Three roles, one recursive process
The Planning agent constructs and revises the plan. The Lean agent implements one statement and uses compiler feedback to repair its proof. A separate Check agent examines an artifact independently, answering one question at a time: is the statement mathematically sound, should a stuck step be decomposed, or does a clean build still prove the intended statement?
A failure can therefore change the decomposition rather than only trigger another tactic attempt. In the paper's Burnside theorem example, an initial six-node plan grows to 32 nodes as difficult claims are split into smaller obligations. The system then closes those obligations and works back toward the anchored target.
What counts as a completed proof
Compilation alone is not the completion criterion. The benchmark protocol also requires preservation of the original theorem signature and a transitive audit of its axioms. That audit excludes sorryAx, which represents an unproved placeholder, and permits only Lean's standard propext, Quot.sound, and Classical.choice axioms.
The reported harness uses general-purpose models without fine-tuning, a custom reinforcement-learning objective, or theorem-specific scaffolding. The experiment tests how planning, feedback, and verification can organize the capabilities of an existing model.
Results and their limits
The FormalQualBench result includes one run beyond the four-hour budget, as noted above. Putnam timing comparisons use other systems' published results. A separate stability study repeated four selected qualifying-exam problems eight times each; all 32 attempts produced clean proofs. This does not establish repeatability across the full benchmark.
Performance still depends on the reasoning model and the availability of usable Mathlib results. Recursive replanning and repeated context reads also increase inference cost. The current software has expanded into exploration, formalization, and paper-writing workflows; those capabilities should be distinguished from the harness configuration evaluated in the paper.
Result
The paper reports 10/23 FormalQualBench problems solved: nine within four hours and one in an extended 4h40m run. The same harness solves all 12 Putnam 2025 problems, with 789 minutes of summed wall-clock time.
What remains
Reduce redundant compilation and repeated planning, explore less expensive models, and use failed decompositions to identify gaps in the supporting mathematical library.
Paper & resources
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
Jinzheng Li, Zeru Zhu, and Yuanjie Ren
arXiv:2605.26959 · Preprint