Over our first few months we have been building AxiomProver, an autonomous AI theorem prover that produces formal Lean proofs to mathematical problems. To benchmark progress, we participated in Putnam 2025, the world’s hardest college-level math test.
The Putnam exam took place on December 6th. Here at Axiom, the humans behind AxiomProver gathered for a Putnam-solving party. We received the problems in real-time, section by section, from an official Putnam proctor after each part began. AxiomProver had autonomously and fully solved 12 out of 12 problems using the formal verification language Lean, 8 of which within the exam time (by 16:00 PT, December 6th).
Today, we release the proofs generated by AxiomProver, and provide commentary on the mathematics behind these solutions, roughly gro…
Over our first few months we have been building AxiomProver, an autonomous AI theorem prover that produces formal Lean proofs to mathematical problems. To benchmark progress, we participated in Putnam 2025, the world’s hardest college-level math test.
The Putnam exam took place on December 6th. Here at Axiom, the humans behind AxiomProver gathered for a Putnam-solving party. We received the problems in real-time, section by section, from an official Putnam proctor after each part began. AxiomProver had autonomously and fully solved 12 out of 12 problems using the formal verification language Lean, 8 of which within the exam time (by 16:00 PT, December 6th).
Today, we release the proofs generated by AxiomProver, and provide commentary on the mathematics behind these solutions, roughly grouped into three categories:
I. Problems that were easy for humans but painstaking when it comes to formalization
II. Problems that AxiomProver cracked surprisingly while humans didn’t expect it to
III. Problems where AxiomProver and humans solved via different math approaches