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.
MerLean
A fully automated agentic framework for autoformalization — bridging LaTeX research papers and verified Lean 4 code.
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.
Videos
Demos and presentations showcasing MerLean in action.
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.