Primary evidence
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal MathematicsS1 · Primary research · Paper · 2026-01-20
- Numina-Lean-Agent implementation and proof resourcesS1 · Primary research · Repository
Numina-Lean-Agent turns a general coding agent into an open Lean mathematics reasoner
The system uses a general-purpose coding-agent loop as the controller for Lean work and extends it with theorem retrieval, informal proving, verification and auxiliary reasoning tools exposed through an MCP-oriented interface.
What happened?
The paper reported that Numina-Lean-Agent, built around Claude Code and Numina-Lean-MCP, solved all 12 Putnam 2025 problems with Claude Opus 4.5 and was also used with mathematicians to formalize the Effective Brascamp–Lieb theorem; the agent implementation and formal solutions were released publicly.
The system uses a general-purpose coding-agent loop as the controller for Lean work and extends it with theorem retrieval, informal proving, verification and auxiliary reasoning tools exposed through an MCP-oriented interface. Its public repository includes setup instructions, runnable agent tooling and links to the Putnam proof artifacts.
Why it matters
The work connected the rapidly developing coding-agent ecosystem to formal mathematics and suggested that improvements in general agent harnesses and base models could transfer directly into theorem proving without rebuilding a bespoke prover stack for each task.
Significance rationale: Numina-Lean-Agent showed a distinct formal-mathematics architecture in which a general coding agent could directly operate Lean and call specialized tools through MCP, rather than depending on a task-specific prover pipeline or newly trained formal model.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Autonomous primary role
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Hybrid
- AI contribution
- The coding agent autonomously inspects Lean goals, edits proof code and invokes specialized reasoning and retrieval tools; Lean compiler feedback mechanically constrains accepted formal outputs.
- Human contribution
- Researchers designed the agent and MCP tool interface, configured evaluation tasks, released the implementation and proof artifacts, and supplied mathematician collaboration and semantic oversight in the research-level formalization case.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- numina-lean-agent, claude-code, numina-lean-mcp, lean
- Organizations
- project-numina
- Problems
- putnam-2025, effective-brascamp-lieb-formalization
- Methods
- coding-agent, model-context-protocol, compiler-feedback, theorem-retrieval, lean
Sources & artifacts
- Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal MathematicsS1 · Primary research · Paper · accessed 2026-09-11
- Numina-Lean-Agent implementation and proof resourcesS1 · Primary research · Repository · accessed 2026-09-11
- Numina-Lean-Agent implementation and Lean proof resourcesArtifact · Code
Verification history
- 2026-01-20 · Paper released · E2 · Research record
The arXiv paper introduced the general coding-agent paradigm for formal mathematics and reported the Putnam 2025 and Brascamp–Lieb results.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
The public Numina-Lean-Agent repository exposes runnable tooling and links to generated Lean proof artifacts. Machine-checked describes Lean acceptance of formal outputs; it does not mean Chronicle independently reproduced every reported run or judged the informal-to-formal correspondence.
Corrections
No corrections recorded.