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.
Figures & tables
Paper
Statements
Lines of Lean
Declarations
Time
Balanced Product
44
14,997
730
20h 4m
Fault-Tolerant QC
47
18,557
923
11h 41m
Quantum Topology
23
7,761
397
7h 51m
Table 1: Summary of formalization experiments per paper.
Type
Count
Avg. Time
Avg. Compiles
Definition
49
18m 0s
11.7
Theorem
15
39m 41s
22.4
Lemma
20
33m 22s
18.3
Remark
26
10m 34s
7.1
Corollary
4
19m 23s
5.5
Total/Avg
114
21m 54s
13.0
Table 2: Formalization statistics by statement type across all three papers.
Figure 2: Distribution of compile attempts by statement type for each paper (maximum 30 attempts before axiom phase). Most statements resolve within 1–10 attempts; theorems and lemmas require significantly more iterations.
Department of Statistics, University of Warwick, UK · Center for Advanced Intelligence Project, RIKEN, Japan · Department of Statistics, University of Michigan, USA +3