Research map / Multi-agent systems and games / LLM agents
Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes using a general coding agent (Claude Code) plus an MCP tool suite (Numina-Lean-MCP) as a formal math reasoner, achieving 12/12 on Putnam 2025 and assisting formalization of Brascamp-Lieb inequalities.
Problem
Existing agentic formal theorem provers rely on task-specific pipelines and trained formal provers, limiting flexibility and reproducibility; the paper asks whether a general coding agent can serve as an open, general formal math reasoner.
Approach
Use a general coding agent (Claude Code) with MCP-exposed Lean tools (Lean-LSP-MCP, LeanDex semantic theorem search, an informal prover, and a discussion-partner tool) so performance scales by swapping the base model without training; add blueprint-driven planning and subagents for long-horizon formalization.
Key results
- Numina-Lean-Agent with Claude Opus 4.5 solved 12/12 Putnam 2025 problems, matching AxiomProver and surpassing Aristotle by two problems.
- Iterative refinement for the informal prover outperformed independent sampling on Putnam 2025 B4 (completed in 5 rounds vs. failing within 10 for sampling).
- Human-AI collaboration formalized over 8,000 lines of Lean for Effective Brascamp-Lieb inequalities in under two weeks, with about 70 agent-introduced definitions and lemmas.
Surprising findings
- The agent autonomously revised an incorrect formal statement during formalization instead of only attempting to prove the statement or its negation.
Limitations
- Generated Lean code is often overly long, verbose, and less well-structured than Mathlib-idiomatic code.
- Struggles with type-level issues (e.g., Real to NNReal conversions) that slow or block proofs.
- Proof length is generally longer than step-based provers such as Aristotle.
Experimental setup
Datasets: Putnam 2025 formal statements (from Seed-Prover 1.5) Mathlib
Benchmarks: Putnam 2025
Metrics: problems solved (out of 12) solving time (minutes) proof length (lines of Lean code)
Baselines: Aristotle Seed-Prover 1.5 AxiomProver
Builds on: Lean-LSP-MCP LeanExplore Gemini IMO agent Claude Code
Closest papers by meaning
- A Minimal Agent for Automated Theorem Proving (ICML 2026 · similarity 0.91)
- LeanAgent: Lifelong Learning for Formal Theorem Proving (ICLR 2025 · similarity 0.89)
- HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMs (ICML 2026 · similarity 0.89)
- ImProver: Agent-Based Automated Proof Optimization (ICLR 2025 · similarity 0.89)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.88)
- Position: Formal Mathematical Reasoning—A New Frontier in AI (ICML 2025 · similarity 0.88)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.