AxiomProver at Putnam 2025

Putnam 2025, the world's hardest college-level math test, ended December 6th. By the end of the competition, AxiomProver had solved 8 out of 12 problems. In the following days, it solved the remaining 4. AxiomProver is an autonomous multi-agent ensemble theorem prover for Lean 4.21.0, developed by Axiom Math.

This repository contains the solutions generated by AxiomProver. Asterisk denotes solutions found after the competition.

1. 2025 A1: [source], [graph]. Prover: 110 minutes, 7M tokens. Proof: 652 lines, 23 theorems, 561 tactics.
2. 2025 A2: [source], [graph]. Prover: 185 minutes, 6M tokens. Proof: 556 lines, 26 theorems, 581 tactics.
3. 2025 A3: [source], [graph]. Prover: 165 minutes, 8M tokens. Proof: 1,333 lines, 78 theorems, 1,701 tactics.
4. 2025 A4: [source], [graph]. Prover: 107 minutes, 8M tokens. Proof: 960 lines, 32 theorems, 1,107 tactics.
5. 2025 A5*: [source], [graph]. Prover: 518 minutes, 9.1M tokens. Proof: 2,054 lines, 52 theorems, 3,074 tactics.
6. 2025 A6*: [source], [graph]. Prover: 259 minutes, 16M tokens. Proof: 588 lines, 28 theorems, 670 tactics.
7. 2025 B1: [source], [graph]. Prover: 270 minutes, 7M tokens. Proof: 1,386 lines, 49 theorems, 1,841 tactics.
8. 2025 B2: [source], [graph]. Prover: 65 minutes, 2M tokens. Proof: 417 lines, 28 theorems, 325 tactics.
9. 2025 B3: [source], [graph]. Prover: 43 minutes, 2.9M tokens. Proof: 340 lines, 11 theorems, 422 tactics.
10. 2025 B4*: [source], [graph]. Prover: 112 minutes, 249K tokens. Proof: 1,061 lines, 23 theorems, 1,433 tactics.
11. 2025 B5: [source], [graph]. Prover: 354 minutes, 18M tokens. Proof: 1,495 lines, 66 theorems, 1,967 tactics.
12. 2025 B6*: [source], [graph]. Prover: 494 minutes, 21M tokens. Proof: 1,019 lines, 30 theorems, 1,052 tactics.

To compile and verify these solutions using SafeVerify, run:

$ lake run verify
Verifying A1 solution ... ✅
Verifying A2 solution ... ✅
Verifying A3 solution ... ✅
Verifying A4 solution ... ✅
Verifying A5 solution ... ✅
Verifying A6 solution ... ✅
Verifying B1 solution ... ✅
Verifying B2 solution ... ✅
Verifying B3 solution ... ✅
Verifying B4 solution ... ✅
Verifying B5 solution ... ✅
Verifying B6 solution ... ✅

License

This repository is licensed under the MIT License. See LICENSE for details.

The Team

Prover leads: Chris Cummins, GasStationManager.

Engineering: Dejan Grubisic, Leopold Haller, Andranik Kurghinyan, Aram Markosyan, Manooshree Patel, Gaurang Pendharkar, Vedant Rathi, Alex Schneidman, Volker Seeker, Ishan Sinha, Jimmy Xin.

Mathematics: Evan Chen, Ben Eltschig, Kenny Lau, Ken Ono, Jujian Zhang.

Leadership: Carina Hong, Hugh Leather, Shubho Sengupta.