Putnam 2025, the world’s hardest college-level mathematics competition, concluded on December 6th, 2025. Numina-Lean-Agent is an autonomous agentic theorem proving system which combines Claude Code with Numina-Lean-MCP to enable autonomous interaction with Lean, retrieval of relevant theorems, informal proving and auxiliary reasoning tools.
This repository contains the Lean formalizations of the Putnam 2025 problems
generated by Numina-Lean-Agent. All solutions are fully verified by Lean.
Reported proof lengths are measured after removing all comments and blank lines
for a fair comparison across provers. We also report the approximate cost upper
bound imposed on the proving process.
Numina-Lean-Agent successfully solved all 12 problems from Putnam 2025.
The table below reports the total proving time (in minutes), the final proof
length (in lines of Lean code), and the associated cost budget (in USD).
| Problem | Time (min) | Proof length (lines) | Cost budget (USD) |
|---|---|---|---|
| 2025 A1 | 97 | 365 | 50 |
| 2025 A2 | 30 | 401 | 50 |
| 2025 A3 | 44 | 422 | 50 |
| 2025 A4 | 169 | 605 | 50 |
| 2025 A5 | 2040 | 3263 | 1000 |
| 2025 A6 | 89 | 835 | 50 |
| 2025 B1 | 55 | 328 | 50 |
| 2025 B2 | 142 | 690 | 50 |
| 2025 B3 | 30 | 292 | 50 |
| 2025 B4 | 308 | 648 | 50 |
| 2025 B5 | 88 | 929 | 50 |
| 2025 B6 | 797 | 1820 | 300 |
All solutions are fully verified by Lean. Importantly, all final proofs depend only on the following three basic axioms:
propextClassical.choiceQuot.sound
No additional classical axioms or nonstandard extensions are assumed.
This repository is licensed under the MIT License. See LICENSE for details.