Source-linked AI summary
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
Junqi Liu, Zihao Zhou, Zekai Zhu, Marco Dos Santos, Weikun He, Jiawei Liu, Ran Wang, Yunzhou Xie, Junqiao Zhao, Qiufeng Wang, Lihong Zhi, Jia Li, Wenda Li
TL;DR
Existing agentic theorem provers often rely on task-specific pipelines, trained formal provers, and limited implementation access, motivating a more flexible and reproducible approach. The paper uses a general coding agent with MCP-based Lean and reasoning tools, and reports 12 / 12 Putnam 2025 solutions plus collaborative Brascamp-Lieb formalization. Generated proofs can remain verbose, poorly structured, or slowed by type-level requirements, leaving formal elegance and robustness as limitations.
Problem
Existing agentic proving systems rely on task-specific pipelines, extensively trained formal provers, or limited implementation details, restricting extensibility and reproducibility.
Method
The paper builds Numina-Lean-Agent from Claude Code and Numina-Lean-MCP, enabling autonomous selection of Lean, theorem-retrieval, informal-proving, and auxiliary reasoning tools.
Results
Numina-Lean-Agent solved 12 / 12 Putnam 2025 problems with Claude Opus 4.5 and collaboratively formalized the Brascamp-Lieb theorem.
Takeaways & Limitations
The system supports both automated theorem proving and sustained human–machine formalization, including large-scale Lean-library extension.
Takeaways & Limitations
Generated formalizations may be verbose and poorly structured, while type-level constraints can substantially slow or derail proofs.
Abstract
from arXiv · showhide
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.
1. Introduction
Existing agentic proving systems achieve strong performance but often depend on task-specific pipelines, trained formal provers, and limited-access implementations. Numina-Lean-Agent instead uses a general coding agent with extensible tools and reports state-of-the-art Putnam 2025 performance.
- Existing agentic proving systems combine formal environments, models, and tools but remain limited by task-specific designs and trained provers.These constraints can limit extensibility to new tools or domains.
- Most existing systems are closed-source with limited implementation details, hindering community reproduction and extension.
- Numina-Lean-Agent builds a formal math reasoner from a general coding agent, whose interface supports diverse proof-engineering tasks beyond proving.Its design also supports replacing the underlying base model without training and autonomously invoking specialized MCP tools.
- 12 / 12 Putnam 2025 problems were solved using Claude Opus 4.5, matching AxiomProver and surpassing Harmonic’s Aristotle by two problems.The paper also reports a collaborative formalization of the Brascamp-Lieb theorem.
2. Numina-Lean-Agent
Numina-Lean-Agent combines Claude Code with MCP tools that support Lean interaction, theorem retrieval, informal proof generation, and auxiliary discussion. Its architecture lets the agent select tools and explore proof strategies through compiler feedback and semantic search.
- 2.1. Overview: Numina-Lean-Agent is built on Claude Code and Numina-Lean-MCP, dynamically selecting tools for diverse formal reasoning queries.
- 2.2. Numina-Lean-MCP: Lean-LSP-MCP connects language models to Lean through LSP, providing semantic awareness, goal inspection, diagnostics, code execution, and strategy exploration.
- 2.2. Numina-Lean-MCP: Lean’s execution tools create a trial-feedback-optimization loop by compiling snippets and evaluating multiple proof strategies in parallel.
- 2.2. Numina-Lean-MCP: Local search and Lean Loogle retrieve definitions and theorems from Lean projects, the standard library, and Mathlib using natural-language or structured queries.The dual-retrieval mechanism is intended to ensure cited theorems exist and fit the context.
- 2.2. Numina-Lean-MCP: LeanDex uses an intelligent agent to interpret natural-language queries and retrieve relevant Lean objects across packages including mathlib and FLT.It extends LeanExplore with enhanced reasoning and retrieval capabilities.
- 2.2. Numina-Lean-MCP: The Informal Prover iteratively refines generated solutions through interaction between a Generator and a Verifier.Each candidate is independently verified three times and accepted only when all passes judge it correct.
- 2.2. Numina-Lean-MCP: The Discussion Partner lets Claude Code consult other language models when proof bottlenecks, strategy choices, or intermediate-lemma ambiguities arise.
3. Evaluation
Numina-Lean-Agent solves all 12 Putnam 2025 problems under sequential, no-internet evaluation and shows efficiency advantages in solving time and proof length. Additional experiments examine iterative versus independent informal proving and use subagents to address long-context difficulties.
- Benchmark performance: 12 out of 12 Putnam 2025 problems were solved under strictly sequential execution with internet search disabled.The evaluation used formal statements provided by Seed-Prover 1.5 and included no parallelization.
- Design comparison: Iterative refinement and independent sampling use the same total number of informal_prover calls in the Putnam 2025 B4 comparison.The two paradigms differ in whether solutions are repeatedly revised or generated independently.
- Solving time: Numina-Lean-Agent achieves shorter solving times than competing methods on several Putnam 2025 problems despite operating without parallel execution.Table 3 reports per-problem solving time in minutes.
- Proof length: Shorter proofs are produced on a substantial number of problems than by AxiomProver and Seed-Prover 1.5, especially on A3, B1, and B5.Compared with Aristotle, whose step-based approach favors very short proofs, Numina-Lean-Agent generally produces longer proofs.
- Subagent mechanism: A5 uses subagents to decompose the proof into independently solved subgoals, addressing difficulties associated with excessively long contexts.The strategy isolates a repeatedly problematic lemma and handles it separately.
4. Formalizing Brascamp Lieb with Numina-Lean-Agent
Numina-Lean-Agent formalizes the Effective Brascamp–Lieb inequalities through blueprint-guided, human–machine collaboration and iterative Lean feedback. The case study demonstrates sustained formalization, adaptive proof decomposition, statement revision, and practical limitations in generated code.
- 4.1. Blueprint Generation: Blueprints decompose complex Lean goals into verifiable subgoals and record dependencies among definitions, intermediate lemmas, and the final theorem.The workflow uses the blueprint as an explicit planning layer rather than proving the final statement directly.
- 4.1. Blueprint Generation: Blueprints are recursively refined when Lean feedback exposes incorrect, underspecified, or poorly granular proof steps.The agent may strengthen assumptions, rephrase statements, or insert intermediate lemmas before continuing formalization.
- 4.2. Human-AI Cooperation: Two human experts and the agent completed more than 8,000 lines of Lean code in less than two weeks of intermittent collaboration.The framework lets mathematicians provide hints and modify the Blueprint during formalization.
- 4.2. Human-AI Cooperation: The agent autonomously introduced approximately 70 definitions, lemmas, and theorems, extending the formal library during the collaboration.This illustrates participation in large-scale, sustained formalization efforts.
- 4.2. Human-AI Cooperation: For involved arguments, the agent sometimes inserted finer-grained intermediate lemmas than those in the original blueprint.The authors describe this as adaptive proof decomposition tailored to formal verification.
- 4.2. Human-AI Cooperation: The agent can inspect statement validity during formalization and autonomously revise an incorrect statement.This extends its role beyond proving a fixed theorem statement.
- 4.3. Limitation: For complete lemma proofs, generated Lean code may become verbose and less structured, especially on larger or more intricate tasks.Local gaps within well-structured proofs were generally handled with higher-quality code.
- 4.3. Limitation: Type-level issues can significantly slow proof development, including failures caused by conversions from Real to NNReal.Handling conversions in advance enabled completion of the remaining proof in the reported case.
A.1. Formal statement of the main theorem of the Effective Brascamp–Lieb inequalities.
The appendix states an upper-bound theorem for finite-dimensional normed and inner-product spaces under metric, positivity, and essential-rank assumptions.
- A.1. Formal theorem statement: The theorem defines an upper bound for a quantity involving the operator norm of a weighted sum of composed maps.Its hypotheses include finite index types, finite-dimensional spaces, positive α values, and a metric-perception condition.
- A.1. Formal theorem statement: The displayed Lean theorem includes products over indices and powers involving dimension, weights, α, acuity, β, and operator norms.The bound is encoded directly as a machine-checkable Lean proposition.
A.2. Self-Correction of Formal Statements during Formalization.
The appendix addresses the zero-dimensional case by stating an empty-space upper-bound lemma with β constrained to zero.
- A.2. Self-Correction of Formal Statements: The empty-case lemma handles the degenerate situation in which the base space has dimension 0.The accompanying comment states that the inequality then holds trivially after both sides simplify.
- A.2. Self-Correction of Formal Statements: The formal statement explicitly assumes that β = 0 when the index type for the base space is empty.This added condition is presented as necessary for the inequality to hold in the empty case.