# MerLean: An Agentic Framework for Autoformalization in Quantum Computation

arXiv: https://arxiv.org/abs/2602.16554 · HTML: https://mlsanity.com/paper/2602.16554/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Placed in Medical and scientific domain agents, one of 16 directions in LLM agents and tool use.
- Builds on 13 of its 23 references that are in the map.
- First posted on arXiv 18 Feb 2026.

## Placed in

- LLM agents and tool use / [Medical and scientific domain agents](https://mlsanity.com/agents/medical-and-scientific-domain-agents/)

## Builds on (most cited first, 13 of 13)

- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics](https://mlsanity.com/paper/2510.12787/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization](https://mlsanity.com/paper/2507.06181/) (2025)
- [A Formalization of the Generalized Quantum Stein's Lemma in Lean](https://mlsanity.com/paper/2510.08672/) (2025)
- [Agentic Proof Automation: A Case Study](https://mlsanity.com/paper/2601.03768/) (2026)
- [PhysProver: Advancing Automatic Theorem Proving for Physics](https://mlsanity.com/paper/2601.15737/) (2026)

## Built on by (most cited first, 10 of 10)

- [Prove2Me: An Open Collaborative Platform for Scaling Math Formalization](https://mlsanity.com/paper/2608.28433/) (2026)
- [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026)
- [Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics](https://mlsanity.com/paper/2606.31134/) (2026)
- [Multi-agent Autoformalization of Tensor Network Theory](https://mlsanity.com/paper/2607.07857/) (2026)
- [AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Language](https://mlsanity.com/paper/2607.16372/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [When AI meets quantum information: A comprehensive review](https://mlsanity.com/paper/2607.00365/) (2026)
- [AutoQuREO: A Framework for Automated Quantum Resource Estimation and Optimization](https://mlsanity.com/paper/2608.12936/) (2026)
- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

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.