MerLean
An Agentic Framework for Autoformalization in Quantum Computation
* Equal contribution
Note: The data in the paper is from an early version of MerLean and does not represent the actual performance of the final product.
Examples
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 — 1450 Lean declarations from 48 statements.
Formalization of Balanced Product Quantum Codes. Covers chain complexes, cohomology, CSS & LDPC codes, expander graphs, Cayley graphs, and the LPS construction — culminating in explicit families of quantum codes with proven distance and rate properties.
Blog
Loading blog posts...
About MerLean
MerLean is a fully automated agentic framework for autoformalization. It 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.
BibTeX
@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}
}