# Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics

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

## Key facts

- Cited by 50 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 6 of its 14 references that are in the map.
- First posted on arXiv 20 Jan 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

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

- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)

## Built on by (most cited first, 30 of 50)

- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics](https://mlsanity.com/paper/2602.24173/) (2026)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [Formalizing Mathematics at Scale](https://mlsanity.com/paper/2605.29955/) (2026)
- [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://mlsanity.com/paper/2603.15929/) (2026)
- [Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement](https://mlsanity.com/paper/2606.06468/) (2026)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [TheoremGraph: Bridging Formal and Informal Mathematics](https://mlsanity.com/paper/2606.25363/) (2026)
- [MechMath Agent Team: LLM Driven Agents for Mathematical Research](https://mlsanity.com/paper/2607.04394/) (2026)
- [Artificial Intelligence and the Structure of Mathematics](https://mlsanity.com/paper/2604.06107/) (2026)
- [Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization](https://mlsanity.com/paper/2606.13925/) (2026)
- [Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics](https://mlsanity.com/paper/2606.31134/) (2026)
- [SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization](https://mlsanity.com/paper/2608.29270/) (2026)
- [QED-Nano: Teaching a Tiny Model to Prove Hard Theorems](https://mlsanity.com/paper/2604.04898/) (2026)
- [Agentic Proving for Program Verification](https://mlsanity.com/paper/2605.23772/) (2026)
- [Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization](https://mlsanity.com/paper/2605.26457/) (2026)
- [Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean](https://mlsanity.com/paper/2606.04883/) (2026)
- [Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts](https://mlsanity.com/paper/2606.03743/) (2026)
- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving](https://mlsanity.com/paper/2603.24465/) (2026)
- [Distilling LLM Feedback for Lean Theorem Proving](https://mlsanity.com/paper/2605.30861/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis](https://mlsanity.com/paper/2606.13782/) (2026)
- [Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory](https://mlsanity.com/paper/2606.20642/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)

## Abstract (arXiv)

Agentic systems have recently become the dominant paradigm for formal theorem proving, achieving strong performance by coordinating multiple models and tools. However, existing approaches often rely on task-specific pipelines and trained formal provers, limiting their flexibility and reproducibility. In this paper, we propose the paradigm that directly uses a general coding agent as a formal math reasoner. This paradigm is motivated by (1) A general coding agent provides a natural interface for diverse reasoning tasks beyond proving, (2) Performance can be improved by simply replacing the underlying base model, without training, and (3) MCP enables flexible extension and autonomous calling of specialized tools, avoiding complex design. Based on this paradigm, we introduce Numina-Lean-Agent, which combines Claude Code with Numina-Lean-MCP to enable autonomous interaction with Lean, retrieval of relevant theorems, informal proving and auxiliary reasoning tools. Using Claude Opus 4.5 as the base model, Numina-Lean-Agent solves all problems in Putnam 2025 (12 / 12), matching the best closed-source system. Beyond benchmark evaluation, we further demonstrate its generality by interacting with mathematicians to successfully formalize the Brascamp-Lieb theorem. We release Numina-Lean-Agent and all solutions at https://github.com/project-numina/numina-lean-agent.