MerLean

AI-assisted workflows for Lean 4 autoformalization, theorem proving, and machine-checked verification.

Yuanjie Ren

MIT

Jinzheng Li

Northeastern University

Yidi Qi

Northeastern University

About MerLean

MerLean began as a bidirectional autoformalization pipeline: it extracts mathematical statements from LaTeX, formalizes them into Lean 4 code built on Mathlib, and translates the result back into human-readable LaTeX for semantic review.

The newer MerLean-Prover work extends that stack into end-to-end Lean theorem proving. A simple recursive looping harness closes 10/23 FormalQualBench problems and 12/12 on a Putnam 2025 slice, without fine-tuning or theorem-specific scaffolding.

2,050+

Lean Declarations

10/23

FormalQualBench

12/12

Putnam 2025 Slice

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.

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

Jinzheng Li*, Zeru Zhu*, Yuanjie Ren*

arXiv preprint arXiv:2605.26959 · cs.LO

arXiv PDF

* Equal contribution.

arXiv 2026

MerLean: An Agentic Framework for Autoformalization in Quantum Computation

Yuanjie Ren*, Jinzheng Li*, Yidi Qi*

arXiv preprint arXiv:2602.16554 · cs.LO

arXiv PDF

Videos

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.

Blueprint PDF Docs

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.

Blueprint PDF Docs