Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
- Published
- Source
- arXiv
- Paper number
- 125
- Field
- Math Reasoning / Formal Proofs
- arXiv ID
- 2601.14027
Key points
- Existing agentic theorem-proving systems often rely on task-specific reasoning pipelines tightly coupled to heavily trained formal provers.
- Many high-performance automatic theorem provers are closed source, which limits transparency, reproducibility, and broader community progress.
- Existing single-model approaches have struggled with the long-horizon structural reasoning inherent in complex formal systems such as Lean.
- The paper proposes a paradigm in which a general-purpose coding agent, specifically Claude Code, serves as the central orchestrator for formal mathematical reasoning.
- It develops Numina-Lean-Agent, an open and modular system that integrates Claude Code with a comprehensive model context protocol called Numina-Lean-MCP.
- Numina-Lean-MCP includes specialized tools for deep interaction with Lean via Lean-LSP-MCP, semantic theorem retrieval via LeanDex, iterative informal proving via Gemini Generator and Verifier, and multi-model collaboration via Discussion Partner.
Paper links
External research summaries. These are not HDATF publications or measured product results.