MerLean is developed in the open. The MerLeanProver organization on GitHub hosts the open-source release of MerLean — an autonomous Lean 4 + Mathlib theorem-proving system built as Claude Code skills and subagents over a plan graph (Apache-2.0) — together with complete machine-checked formalizations it has produced, such as ACMaxConjecture: a sorry-free, axiom-audited Lean 4 proof of Kolokolnikov's algebraic-connectivity conjecture, verified by two independent proof kernels.
MerLean
AI-assisted workflows for Lean 4 autoformalization, theorem proving, and machine-checked verification.
About MerLean
MerLean is a Lean-based verifier and prover for mathematics and code. As a verifier, it turns mathematical solutions, programs, and AI-generated code into machine-checkable certificates that help certify correctness and catch mistakes; as a prover, MerLean-Prover searches for formal proofs for hard and open problems, and supports vibe coding without hallucination by grounding generated code in formal checks.
MerLean-Prover Results (as of May 2026)
MerLean-Prover uses three agent types around a recursive proof-plan loop: planning, focused artifact checking, and Lean compile / repair. The proof assistant remains the judge; each closed proof passes the Lean kernel and axiom audit described in the paper.
Lean Eval top submitters
| Rank | Submitter | Solved |
|---|---|---|
| 1 | Seed Prover (ByteDance) | 62 |
| 2 | Aleph Prover(logicalintelligence.com) | 56 |
| 3 | Aristotle (Harmonic) | 52 |
| 4 | Stealth Model | 42 |
| 5 | MerLean-Prover | 24 |
| 6 | Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) | 21 |
| 7 | Claude Opus 4.7 (1M context) | 17 |
| 8 | GPT-5.5 | 16 |
| 9 | EVO (deepthought.com.au) | 3 |
| 10 | GPT-5.5 Codex | 2 |
Source: Lean Eval public leaderboard, fetched June 12, 2026. Ranked by main benchmark problems solved; internal test problems do not count toward the score.
On the public Lean Eval Benchmark, MerLean-Prover is currently ranked top #5 by main benchmark problems solved: 24 solved problems from a small academic team competing on the same table as large company-backed Lean agents.
FormalQualBench closure rate
| System | Solved / 23 |
|---|---|
| MerLean-Prover (ours) | 10† |
| OpenGauss | 8 |
| Aristotle* | 6 |
| Claude Code (Skills) | 5 |
| Codex | 5 |
| opencode (Opus) | 5 |
| Claude Code | 4 |
| Claude Code (MCP) | 3 |
| Codex (Skills + MCP) | 3 |
† Nine solves close within the 4-hour budget; one extended run closes in 4h40m. *Aristotle results are reported but unvalidated in the benchmark source.
Putnam 2025 wall-clock time (minutes)
| Prob. | Arist. | Seed 1.5 | Axiom | NLA | Ours |
|---|---|---|---|---|---|
| A1 | 30 | 60 | 110 | 97 | 27 |
| A2 | 60 | 30 | 180 | 30 | 31 |
| A3 | 30 | 120 | 165 | 44 | 44 |
| A4 | 180 | 240 | 107 | 169 | 38 |
| A5 | -- | -- | 518 | 2040 | 235 |
| A6 | 60 | 240 | 259 | 89 | 25 |
| B1 | 150 | 540 | 270 | 55 | 161 |
| B2 | 25 | 360 | 65 | 142 | 55 |
| B3 | 40 | 30 | 43 | 30 | 16 |
| B4 | -- | 120 | 112 | 308 | 53 |
| B5 | 420 | 240 | 254 | 88 | 43 |
| B6 | 180 | 180 | 494 | 797 | 61 |
| Solved | 10/12 | 11/12 | 12/12 | 12/12 | 12/12 |
| Total | -- | -- | 2577 | 3889 | 789 |
Comparison columns are reproduced from Numina-Lean-Agent Table 3. Bold cells in the paper mark fastest solves; here they are highlighted.
Cite
@article{ren2026merlean,
title = {MerLean: An Agentic Framework for Autoformalization
in Quantum Computation},
author = {Ren, Yuanjie and Li, Jinzheng and Qi, Yidi},
journal = {arXiv preprint arXiv:2602.16554},
year = {2026},
eprint = {2602.16554},
archivePrefix = {arXiv},
primaryClass = {cs.LO},
doi = {10.48550/arXiv.2602.16554}
}
@misc{li2026merleanproverrecursiveloopingharness,
title = {MerLean-Prover: A Recursive Looping Harness for
Lean 4 Theorem Proving},
author = {Jinzheng Li and Zeru Zhu and Yuanjie Ren},
year = {2026},
eprint = {2605.26959},
archivePrefix = {arXiv},
primaryClass = {cs.LO},
url = {https://arxiv.org/abs/2605.26959}
}
@misc{zhu2026maximizingalgebraicconnectivity2n2,
title = {Maximizing Algebraic Connectivity with $2(n-2)$ Edges:
The Large Vertex Number Case},
author = {Zeru Zhu and Jinzheng Li and Yuanjie Ren and Ji Liu},
year = {2026},
eprint = {2608.07360},
archivePrefix = {arXiv},
primaryClass = {math.CO},
url = {https://arxiv.org/abs/2608.07360}
}
Publications
Research papers from the MerLean project.
arXiv 2026
Maximizing Algebraic Connectivity with 2(n−2) Edges: The Large Vertex Number Case
arXiv preprint arXiv:2608.07360 · math.CO
arXiv 2026
MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
arXiv preprint arXiv:2605.26959 · cs.LO
* Equal contribution.
Blog
Updates on autoformalization, Lean 4, and quantum computation.
Examples
Browse the formalization output produced by MerLean.
Fault-Tolerant Quantum Computation
Formalization of Low-overhead fault-tolerant quantum computation by gauging logical operators. Covers stabilizer formalism, Pauli algebra, transversal gates, gauging graphs, and fault-tolerant measurement — 1,450 Lean declarations from 48 statements.
Balanced Product Quantum Codes
Formalization of Balanced Product Quantum Codes. Covers chain complexes, cohomology, CSS & LDPC codes, expander graphs, Cayley graphs, and the LPS construction.
Maximizing Algebraic Connectivity (ACMAX Conjecture)
Complete Lean 4 proof of Kolokolnikov's conjecture accompanying Maximizing Algebraic Connectivity with 2(n−2) Edges: The Large Vertex Number Case (arXiv:2608.07360): among all graphs on n vertices with 2(n−2) edges, K2,n−2 maximizes algebraic connectivity, for every n ≥ 4 — ~163,000 lines of Lean across 429 modules, sorry-free, axiom-audited, and checked by two independent proof kernels.
Collaborate
An open board for research pairing: post a project you'd like help with, or offer to contribute to one.
This board is offered as an open communication platform for the research community. Projects posted here are independent of MerLean, and need not involve MerLean-Prover or Lean 4 in any way.
Platform license. The Collaborate platform — this page's markup, scripts, styles, and reference server — is © 2026 Yuanjie (Collin) Ren, released under the MIT License; the page's own text and graphics are under CC BY 4.0. You are welcome to copy, reuse, or adapt the platform without asking permission, as long as you keep the copyright and license notice (attribution).
Projects and contribution offers posted to this board remain the copyright of their respective authors and are not covered by these licenses. This notice applies to the Collaborate page only, not to the rest of this site. Licensing questions: collin.yuanjie.ren@gmail.com.
