MerLean: An Agentic Framework for Autoformalization in Quantum Computation

TL;DR

MerLean is an automated framework that extracts, formalizes, and verifies quantum computing statements from LaTeX documents, streamlining formalization and review processes in advanced research.

Contribution

It introduces MerLean, a novel agentic system that automates the entire autoformalization process in quantum computation using Lean 4 and Mathlib.

Findings

Successfully formalized 114 statements into 2,050 Lean declarations.

Achieved end-to-end formalization on three quantum computing papers.

Reduced verification effort to only new definitions and axioms.

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.