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.

Paper on arXiv Paper PDF MerLean website Source code

Year: 2026
Status: Preprint
Topics: LLM agents · Formal verification · Lean

The project in brief

How can an AI agent complete a long formal proof while preserving the mathematical claim it set out to prove?

A long formal proof is also a changing collection of mathematical obligations: which lemmas are needed, what each one assumes, and how they fit together. MerLean-Prover makes that collection explicit, so a failed attempt can lead to a better decomposition.

The example here is Burnside’s theorem on transitive permutation groups of prime degree. Following its proof plan shows why generating Lean code, preserving a mathematical statement, and verifying a finished proof are distinct tasks. The results below describe the public paper’s evaluated harness.

MerLean: anchored theorem, recursive proof plan, and independent verification

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.

Objective

Construct a proof of the original proposition

$\Gamma$ contains the original parameters and hypotheses; $T$ is the target proposition and $p$ its proof term. The proof plan may change, but the original declaration must remain fixed. A successful run also passes a transitive audit of the axioms used by $p$ .

\text{Given }\Gamma\vdash T : \mathrm{Prop},\qquad\text{construct }p\text{ such that }\Gamma\vdash p:T.

MerLean-Prover, arXiv:2605.26959v2 (27 May 2026) · §§2, 4; notation introduced for this explanation

Question: How can an agent revise a long proof without changing the theorem it was asked to prove?
Method: A shared dependency plan, three focused agent roles, and separate checks for mathematical correctness, useful decomposition, and statement preservation.
Progress: 10/23 FormalQualBench solves, including one extended run; 12/12 Putnam 2025 solves. A public Burnside trace makes the recursive process inspectable.

Explore the project

01 / Problem

↳

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.

Papers & resources