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.
21/179Top 5/6
Lean Eval Benchmark
10/23Top 1
FormalQualBench
12/12, 789 minsTop 1
Putnam 2025 Slice
Fundraising, Advisors & Cofounders
We are speaking with pre-seed investors who are interested in capital-efficient assurance infrastructure for AI-generated critical code, formal verification, and machine-checkable scientific and software work.
Pre-seed investors
We are looking for partners who understand deep technical products, early research-to-product transitions, and high-trust markets where correctness evidence matters.
Advisors and cofounder-level collaborators
MerLean already has a working proof stack. We are selectively adding advisors and cofounder-level technical collaborators who can make the company stronger in formal verification and LLM post-training for formal reasoning.
MerLean-Prover Results
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.
Source: Lean Eval public leaderboard, fetched June 9, 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 in the top #5/#6 tier among 25 models: 21 solved problems, tied by solved count with the #5 entry, 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
End-to-End 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}
}
Publications
Research papers from the MerLean project.
arXiv 2026
MerLean-Prover: A Recursive Looping Harness for End-to-End Lean 4 Theorem Proving
Demos and presentations showcasing MerLean in action.
MerLean Product Demo (1080p)
A three-minute walkthrough of the MerLean workflow, from research artifact ingestion to machine-checked Lean output and interactive exploration.
Open the video directly.
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.
