MerLean: An Agentic Framework for Autoformalization in Quantum Computation
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866911455259918336 |
|---|---|
| author | Ren, Yuanjie Li, Jinzheng Qi, Yidi |
| author_facet | Ren, Yuanjie Li, Jinzheng Qi, Yidi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_16554 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | MerLean: An Agentic Framework for Autoformalization in Quantum Computation Ren, Yuanjie Li, Jinzheng Qi, Yidi Logic in Computer Science Artificial Intelligence Emerging Technologies Quantum Physics 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. |
| title | MerLean: An Agentic Framework for Autoformalization in Quantum Computation |
| topic | Logic in Computer Science Artificial Intelligence Emerging Technologies Quantum Physics |
| url | https://arxiv.org/abs/2602.16554 |