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.

翻译：我们介绍了MerLean，一个用于量子计算中自动形式化的全自动化智能体框架。MerLean从\LaTeX{}源文件中提取数学陈述，将其形式化为基于Mathlib构建的已验证Lean~4代码，并将结果转换回人类可读的\LaTeX{}格式以进行语义审查。我们在三篇理论量子计算论文上评估了MerLean，从总计114个陈述中生成了2,050个Lean声明。MerLean在所有三篇论文上实现了端到端的形式化，将验证负担降至仅需处理新引入的定义和公理。我们的结果表明，智能体驱动的自动形式化能够扩展到前沿研究领域，既为机器验证的同行评审提供了实用工具，也为挖掘高质量合成数据以训练未来推理模型提供了可扩展的引擎。我们的方法同样可推广至数学和理论物理学的任何其他严谨研究领域。