mlsanityData to 7 Oct 2026

MerLean: An Agentic Framework for Autoformalization in Quantum Computation

arXiv 2602.16554 ↗First posted 18 Feb 2026cs.LO cs.AI cs.ETcited by 8

On the map: LLM agents and tool use → Medical and scientific domain agents

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.

Key facts. Cited by 8 papers in the map (data through 7 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.

Builds on

13 of 23 references.

References · 13

  1. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  2. 2022Autoformalization with Large Language Modelscited by 252
  3. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  4. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  5. 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 43
  6. 2024Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistencycited by 39
  7. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  8. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  9. 2025Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitionscited by 20
  10. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 15
  11. 2025A Formalization of the Generalized Quantum Stein's Lemma in Leancited by 6
  12. 2026Agentic Proof Automation: A Case Studycited by 4
1 more
  1. 2026PhysProver: Advancing Automatic Theorem Proving for Physicscited by 2

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 8.

8 papers.

  1. 2026The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learningcited by 4
  2. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematicscited by 4
  3. 2026Multi-agent Autoformalization of Tensor Network Theorycited by 2
  4. 2026AoA: Theorem Proving Agent over Abstract Syntax Tree of Redesigned Languagecited by 1
  5. 2026Prove2Me: An Open Collaborative Platform for Scaling Math Formalizationcited by 1
  6. 2026AutoQuREO: A Framework for Automated Quantum Resource Estimation and Optimizationcited by 0
  7. 2026AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanicscited by 0
  8. 2026Choir: An Open Protocol for Distributed Multi-Agent Autoformalizationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Agent-Q: Fine-Tuning Large Language Models for Quantum Circuit Generation and Optimization
  2. 2025QHackBench: Benchmarking Large Language Models for Quantum Code Generation Using PennyLane Hackathon Challenges
  3. 2026FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
  4. 2026An LLM System for Autonomous Variational Quantum Circuit Design
  5. 2026Lowering the implementation barrier of neutral-atom quantum computing with agentic workflows
  6. 2026Generative AI for Quantum Circuits and Quantum Code: A Technical Review and Taxonomy
  7. 2025QAgent: An LLM-based Multi-Agent System for Autonomous OpenQASM programming
  8. 2025Enhancing LLM-based Quantum Code Generation with Multi-Agent Optimization and Quantum Error Correction