MerLean

Example: Fault-Tolerant Quantum Computation

This page presents the formalization output for Low-overhead fault-tolerant quantum computation by gauging logical operators produced fully automatically by MerLean. The formalization covers stabilizer formalism, Pauli algebra, transversal gates, gauging graphs, and fault-tolerant measurement — yielding 923 Lean declarations from 47 statements with zero axioms.

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{ren2025merlean,
  title     = {MerLean: An Agentic Framework for Autoformalization
               in Quantum Computation},
  author    = {Ren, Yuanjie and Li, Jinzheng and Qi, Yidi},
  year      = {2026}
}