MerLean

A fully automated agentic framework for autoformalization — bridging LaTeX research papers and verified Lean 4 code.

Read the Paper

Yuanjie Ren

MIT

Jinzheng Li

Northeastern University

Yidi Qi

Northeastern University

About MerLean

MerLean is a bidirectional pipeline powered by Claude that extracts mathematical statements from LaTeX, formalizes them into verified Lean 4 code built on Mathlib, and translates the result back into human-readable LaTeX for semantic review — all without human intervention.

Across three quantum-computing papers (114 statements), MerLean produced 2,050 Lean declarations totaling 41,000+ lines of verified code, achieving full formalization without axioms on two of three papers.

2,050

Lean Declarations

41k+

Lines of Code

114

Statements Formalized

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} }

Publications

Research papers from the MerLean project.

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.

Videos coming soon. Stay tuned for demos and presentations!

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