Source-linked AI summary
MerLean: An Agentic Framework for Autoformalization in Quantum Computation
Yuanjie Ren, Jinzheng Li, Yidi Qi
TL;DR
Research-level mathematical papers still require scalable ways to translate informal statements into machine-checkable proofs while preserving their intended meaning. MerLean addresses this with a bidirectional agentic pipeline that formalizes LaTeX papers in Lean 4 and translates verified code back for semantic review. Across three theoretical quantum-computing papers, it formalized 114 statements into 2,050 declarations, while exposing library gaps through explicit axioms.
Problem
Theoretical quantum computation faces a verification bottleneck as research volume grows and specialized mathematical machinery remains incompletely represented in formal libraries.
Method
MerLean uses agentic extraction, iterative compile-fix formalization, faithfulness checking, and reverse translation from verified Lean 4 libraries into human-readable LaTeX.
Results
114 statements across three papers became 2,050 Lean declarations, and all three papers were successfully formalized end to end.
Takeaways & Limitations
The results demonstrate that fully automated formalization of frontier research is feasible while allowing domain experts to review semantic alignment without formal-methods expertise.
Takeaways & Limitations
Formalizations may require explicit axioms for mathematical machinery not yet available in Mathlib, including spectral sequences and Künneth isomorphisms.
Abstract
from arXiv · showhide
We introduce MerLean, a fully automated agentic framework for autoformalization in quantum computation. MerLean extracts mathematical statements from \LaTeX{} source files, formalizes them into verified Lean~4 code built on Mathlib, and translates the result back into human-readable \LaTeX{} for semantic review. We evaluate MerLean on three theoretical quantum computing papers producing 2,050 Lean declarations from 114 statements in total. MerLean achieves end-to-end formalization on all three papers, reducing the verification burden to only the newly introduced definitions and axioms. Our results demonstrate that agentic autoformalization can scale to frontier research, offering both a practical tool for machine-verified peer review and a scalable engine for mining high-quality synthetic data to train future reasoning models. Our approach can also be generalized to any other rigorous research in mathematics and theoretical physics.
1 INTRODUCTION
MerLean addresses the growing challenge of verifying rigorous theoretical quantum-computing research by fully automating statement extraction and formalization, then enabling human semantic review. Evaluated on three papers, it formalized all of them and is presented as applicable beyond quantum computation.
- 11,891 quant-ph articles in 2025 illustrate the verification bottleneck facing theoretical quantum computation.
- MerLean automatically extracts, organizes, and formalizes mathematical statements from LaTeX source files without human intervention during formalization.
- Three theoretical quantum-computing papers were evaluated, including one unpublished manuscript and two previously published works.
- MerLean achieved end-to-end formalization on all three papers, adding definitions and axioms when required mathematical machinery was unavailable in Mathlib.
- The framework is presented as extending beyond quantum computation to disciplines that rely on formal mathematical proofs.
2 RELATED WORKS
Related work has established LLM-assisted and agentic theorem proving across mathematics and specialized domains. MerLean shares the generate-check-refine paradigm but targets fully automated, end-to-end formalization of complete research papers.
- LLM-based autoformalization has expanded from competition-level problems to proof-detail expansion, faithfulness verification, and domain-specific applications.
- Recent agentic systems combine frontier LLMs with tool integration for interactive theorem proving, including Ax-Prover and a human-guided formalization of System Capless.
- MerLean shares agentic interaction with Lean 4, a generate-check-refine loop, and frontier LLM reasoning with related systems.
- Unlike the described human-guided workflow, MerLean performs full-paper, fully automated end-to-end formalization on its tested domain.
3 FRAMEWORK
MerLean uses a bidirectional workflow: agents extract and iteratively formalize paper statements into verified Lean libraries, then translate the result back into human-readable LaTeX for semantic review. Compilation feedback, faithfulness checks, and explicit axioms support the process when libraries are incomplete.
- 3 FRAMEWORK: MerLean combines autoformalization into verified Lean 4 libraries with autoinformalization back into human-readable LaTeX for expert review.
- 3.1 AUTOFORMALIZATION: Statement extraction records mathematical content, dependencies, identifiers, and available proof sketches in structured JSON.
- 3.1 AUTOFORMALIZATION: Multiple extraction passes refine vague proof descriptions, add intermediate lemmas, and order statements before their dependents.
- 3.1 AUTOFORMALIZATION: Each statement enters a compile-fix loop that generates declarations, parses compiler errors, and revises the Lean code until success or an attempt limit.
- 3.1 AUTOFORMALIZATION: Faithfulness checking tests whether compiled code preserves the original mathematics because type-checking alone can validate a misrepresented theorem.
- 3.1 AUTOFORMALIZATION: When required results are absent from Mathlib, MerLean can replace blocking subgoals with explicit axioms that remain transparent for later completion.
- 3.1 AUTOFORMALIZATION: The decoder uses the formalization model to convert verified Lean libraries into LaTeX that is more accessible than Lean-specific documentation.
4 EXPERIMENTS
MerLean was evaluated on three theoretical quantum computing papers spanning quantum codes, fault-tolerant computation, and quantum topology. Across these projects, it formalized all three papers while exposing compile-time difficulty, agent-discovered intermediate lemmas, and gaps requiring explicit axioms.
- Evaluation Papers: Three papers covered balanced product codes, fault-tolerant quantum computation, and an unpublished quantum-topology manuscript.The first two papers were published, while the quantum-topology manuscript was unpublished to ensure its content had not appeared in LLM training data.
- Overall Results: 114 statements became 2,050 Lean declarations in under 42 hours, with all three papers successfully formalized.Manual review checked that newly introduced definitions and axioms were mathematically accurate and rigorously constructed.
- Compile Effort: Theorems averaged 39m 41s and 22.4 compile attempts, whereas remarks averaged 10m 34s and 7.1 compiles with no axioms required.These results identify theorems as the hardest statement type and remarks as the easiest in the evaluation.
- Axiom Handling: Balanced Product Codes required explicit axioms for 9.1% of statements because spectral-sequence and Künneth machinery was unavailable in Mathlib.The axioms are marked in both the Lean code and generated blueprint, making results that rely on unverified assumptions visible to readers.
- Compile Effort: Most statements compiled within 1–10 attempts, but hard statements formed a long tail requiring 21+ iterations.Theorems and lemmas dominated the high-compile bins, while definitions and remarks clustered in the lower range.
- Qualitative Observations: MerLean introduced auxiliary lemmas bridging geometric, algebraic, and fault-tolerance arguments needed for downstream formal proofs.Examples include an expansion-count identity, a Pauli anticommutation lemma, and a Cheeger-parameter weight inequality.
5 DISCUSSION
MerLean extends automated formalization toward research workflows by addressing Mathlib gaps, checking semantic faithfulness, and supporting peer review, synthetic-data generation, and physics-library development.
- 5.1 CHALLENGES IN MERLEAN: Mathlib lacks some specialized physics concepts, so MerLean represents missing knowledge with explicitly declared axiom nodes.The paper cautions that axioms should neither trivialize derivations nor be too elementary to encode meaningful results.
- 5.1 CHALLENGES IN MERLEAN: The bidirectional faithfulness pipeline helps detect when compiled code misrepresents the source and exposes its logical structure for human review.Compilation success alone is insufficient because formally valid code can still encode a trivial variation or fabricated definition.
- 5.2 FUTURE APPLICATIONS OF MERLEAN: An ambiguous definition in an unpublished Quantum Topology manuscript caused a persistent axiom requirement until the source was corrected.After the constraint was added, MerLean produced a complete formalization, illustrating its use as a research assistant.
- 5.2 FUTURE APPLICATIONS OF MERLEAN: MerLean could support formalized peer review by pairing research drafts with machine-verified guarantees while reviewers focus on novelty and scientific significance.The proposed workflow runs autoformalization locally during drafting and supplements static PDFs with formal repositories.
- 5.2 FUTURE APPLICATIONS OF MERLEAN: MerLean can mine research-grounded natural-language and formal-code pairs for training specialized theorem provers.The paper describes this as a cycle in which verified formalization supplies data for future language-model training.
- 5.2 FUTURE APPLICATIONS OF MERLEAN: MerLean can accelerate physics-library development by extracting reusable definitions and lemmas from formalized research papers.The discussion names PhysLean/HepLean and Lean-QuantumInfo as relevant library efforts.
6 CONCLUSION
MerLean demonstrates fully automated bidirectional formalization of frontier theoretical quantum-computing research, while the paper identifies broader generalizability and benchmarking as future evaluation needs.
- 6 CONCLUSION: Over 2,000 Lean declarations across 41,000+ lines of verified code show that fully automated formalization of frontier research is feasible.The evaluation covered three theoretical quantum-computing papers and used an iterative compile-fix-verify loop without human intervention.
- 6 CONCLUSION: Autoinformalization lets domain experts review semantic alignment without formal-methods expertise.The framework translates verified Lean libraries back into human-readable material for review.
- 6 CONCLUSION: The current testbed benefits from mature Mathlib support for linear algebra and functional analysis.The authors therefore plan evaluation in domains with deeper dependency chains or different foundational structures, including algebraic geometry and number theory.
- 6 CONCLUSION: Existing autoformalization benchmarks focus mainly on isolated theorem statements rather than interconnected full-paper formalization.The authors plan a dedicated benchmark spanning research papers across multiple mathematical domains.
LLM USAGE DISCLOSURE
The paper discloses LLM use in research and writing, while retaining human responsibility for validating contributions and manuscript integrity.
- Research: Claude (Opus 4.5) served as MerLean’s core reasoning engine for extraction, Lean generation, repair, and translation.The reported experimental results were produced by this LLM-based system.
- Research: The authors verified and validated all research contributions produced with LLM assistance.
- Writing: Claude Code assisted with manuscript editing, including typo correction and grammar improvement.The human authors reviewed, verified, and revised the resulting content.
A FORMALIZATION EXAMPLES
The examples show MerLean formalizing fault-tolerant quantum-computation inequalities and the Künneth formula, while introducing helper lemmas, structured definitions, and explicit axioms where proofs depend on unsupported machinery.
- A.2 AGENT-DISCOVERED HELPER LEMMA: The agent-discovered weight_inequality_core lemma formalizes a lower bound connecting cleaned weight, cleaning-set size, boundary size, Cheeger expansion, and code distance.Its proof branches on whether h(G) ≥ 1 and uses arithmetic reasoning to derive the bound.
- A.2 AGENT-DISCOVERED HELPER LEMMA: The helper lemma uses cleaned weight w′, cleaning-set size |S|, boundary size |∂S|, and code distance d as its key quantities.
- A.3 AXIOM EXAMPLE: K ¨UNNETH FORMULA: The Künneth example formalizes an isomorphism between a direct sum of homology tensor products and the homology of the tensor-product complex.The formalization defines the relevant index, source, target, component maps, and final equivalence.
- A.3 AXIOM EXAMPLE: K ¨UNNETH FORMULA: The construction first defines the source and target types, then builds a cycle-level cross product that maps tensor products into cycles of the total complex.The index consists of integer pairs whose sum equals n, and the tensor-product homology spaces provide the component types.
- A.3 AXIOM EXAMPLE: K ¨UNNETH FORMULA: The proof architecture has three stages: constructing the map on cycles, descending it to homology, and establishing bijectivity for the main theorem.The cycle and boundary properties are represented through explicit auxiliary axioms, followed by injectivity and surjectivity assumptions.
- A.3 AXIOM EXAMPLE: K ¨UNNETH FORMULA: Boundary preservation is axiomatized for both boundary–cycle and cycle–boundary tensor products so the cross product descends to homology.These declarations support the well-defined homology map used in the Künneth construction.
- A.3 AXIOM EXAMPLE: K ¨UNNETH FORMULA: The final Künneth map is built componentwise and its injectivity and surjectivity are axiomatized before constructing the linear equivalence.The equivalence is obtained with LinearEquiv.ofBijective from the two bijectivity properties.
A.1 THEOREM: FAULT TOLERANCE OF GAUGING MEASUREMENT
The theorem formalizes fault tolerance for gauging measurement: under expansion and sufficient measurement-round conditions, the spacetime fault-distance equals the original code distance d.
- A.1 THEOREM: FAULT TOLERANCE OF GAUGING MEASUREMENT: The spacetime fault-distance d_ST equals the original code distance d under the theorem’s stated conditions.The conditions are a Cheeger constant h(G) >= 1 and at least d measurement rounds.
- A.1 THEOREM: FAULT TOLERANCE OF GAUGING MEASUREMENT: The formal theorem assumes every spacetime logical fault satisfies a lower-bound case and that a weight-d logical fault exists.These assumptions support the lower and upper bounds needed to establish equality.
- A.1 THEOREM: FAULT TOLERANCE OF GAUGING MEASUREMENT: The proof derives the upper bound d_ST <= d from an explicitly constructed logical fault of weight d.The witness fault satisfies the required logical-fault predicate and has weight cfg.d.
- A.1 THEOREM: FAULT TOLERANCE OF GAUGING MEASUREMENT: The proof derives the lower bound d_ST >= d by selecting a minimum-achieving logical fault and applying the spacetime fault-distance lower-bound theorem.The minimum fault is shown to have the required logical effect, then its weight is bounded below by d.