Numina-Lean-Agent
Numina-Lean-Agent proposes a paradigm shift in automated theorem proving: instead of building complex, multi-component systems with heavy computational overhead, it directly uses a general coding agent as a formal math reasoner. Combining Claude Code with Numina-Lean-MCP, the system autonomously interacts with the Lean proof assistant while accessing theorem libraries and auxiliary reasoning tools.
Ask this paper
General agent over specialized provers: Rather than training task-specific models, the system leverages a general-purpose coding agent. Performance improves simply by upgrading the base model, making the approach accessible and reproducible without expensive retraining pipelines.
MCP-powered tool integration: The system uses Model Context Protocol for flexible extension, including Lean-LSP-MCP for proof assistant interaction, LeanDex for semantic theorem retrieval, and an informal prover for generating detailed proof strategies.
State-of-the-art results: Using Claude Opus 4.5 as the base model, Numina-Lean-Agent solves all 12 problems on Putnam 2025, matching the best closed-source systems. It also successfully formalized the Brascamp-Lieb theorem through direct collaboration with mathematicians.
Open-source release: The full system and all solutions are released on GitHub under Creative Commons BY 4.0, enabling direct reproduction and extension by the research community.