Excited to share our #ICML2026 poster on Numina-Lean-Agent, an open and agentic reasoning system for formal mathematics. If you are at @icmlconf and interested in formal mathematics, theorem proving, agentic systems, or #AIforScience, come visit our poster presented by @ahhwuhu Thursday, July 9 2026 2:30 PM – 4:15 PM Hall A We’d love to chat! #OpenSourceAI #AIagents #Lean4

The core idea is simple: instead of training a theorem-proving-specific pipeline from scratch, we explore whether a general coding agent can be turned into a strong formal mathematics reasoner by giving it the right tools through MCP. Numina-Lean-Agent integrates Lean interaction, semantic theorem retrieval, informal proving, and multi-model discussion. In our experiments, it solves 12/12 Putnam 2025 problems, matching or surpassing several closed-source systems, while remaining #opensource.