Papers With

← All papers
First page of MerLean: An Agentic Framework for Autoformalization in Quantum Computation

MerLean: An Agentic Framework for Autoformalization in Quantum Computation

Yuanjie Ren, Jinzheng Li, Yidi Qi

cs.LO Feb 18, 2026 · v1
autoformalization ai-agents quantum
Read PDF arXiv abstract Code
TL;DR
MerLean autoformalizes quantum-computing paper statements into verified Lean 4 code on Mathlib.
Abstract
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.
Problem

Autoformalization of research-level mathematics into verified Lean 4 code has not been demonstrated at scale for domain-specific fields like quantum computation, and existing methods require significant manual intervention.

Approach

MerLean is a fully automated agentic framework that 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. The framework operates bidirectionally: autoformalization (LaTeX to Lean) and autoinformalization (Lean to LaTeX). It uses iterative compilation attempts with compiler feedback to repair formalization errors.

Results

MerLean produces 2,050 Lean declarations from 114 statements across three theoretical quantum computing papers, achieving end-to-end formalization on all three. Average compilation attempts vary by statement type: 11.7 for definitions, 22.4 for theorems, and 11.4 for lemmas. Total formalization time ranges from 5h 42m to 20h 4m per paper.

PaperStatementsLines of LeanDeclarationsTime
Balanced Product4414,99773020h 4m
Fault-Tolerant----
MerLean results across three quantum computing papers