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
A technical report on AxiomProver is to follow.
Problems that were easy for humans but painstaking when it comes to formalization
Calculus in Lean Can Make You Grumpy
The most approachable Putnam problems tend to be calculus, but formalizing them in Lean can be a pain! Recall the initial days of Mathlib, simple concepts in the first chapter of any analysis textbook took a long time to define. For Putnam 2025, these are the second problem of each section.
A2. Find the largest real number $a$ and the smallest real number $b$ such that \[a\,x(\pi-x)\le \sin x \le b\,x(\pi-x)\] for all $x$ in the interval $[0,\pi]$.
B2. Let $f\colon[0,1]\to[0,\infty)$ be strictly increasing and continuous. Let $R$ be the region bounded by $x=0$, $x=1$, $y=0$, and $y=f(x)$. Let $x_1$ be the $x$-coordinate of the centroid of $R$. Let $x_2$ be the $x$-coordinate of the centroid of the solid generated by rotating $R$ about the $x$-axis. Prove that $x_1 \lt x_2$.
For problem A2, we’ve included a graph of the function $h(x) = \cos(x) - (1 - \frac{4}{\pi^2} x^2)$ along with the formal Lean proof that it’s non-positive on $[0, \pi/2]$. The graph makes this fact obvious at a glance. Then it takes some math to rigorously establish that. However, reading through the Lean code line by line is a much more tedious effort.
For B2, it’s the same story. A simple positivity lemma for a human takes over 60 lines of Lean. A2’s lemma h_nonpos_on_Icc and B2’s lemma psi_support_pos are also the two heaviest nodes in their respective proofs.
Combinatorial Constructions Are Friendly Beasts
At a conversation over the chalkboard at tea time, a combinatorial construction of a problem you got stuck on is shown to you. It often induces some sort of shock - all of a sudden, why does it feel so simple?! Your friend says do this, then that in a couple of sentences and everyone nods along. But the moment one tries to pin that intuition down into a fully formal proof, especially in a proof assistant, things get surprisingly tricky.
A5. Let $n$ be an integer with $n\ge 2$. For a sequence $s=(s_1,\dots,s_{n-1})$ where each $s_i=\pm 1$, let $f(s)$ be the number of permutations $(a_1,\dots,a_n)$ of $\{1,2,\dots,n\}$ such that $s_i(a_{i+1}-a_i)\gt0$ for all $i$. For each $n$, determine the sequences $s$ for which $f(s)$ is maximal.
Take Problem A5 as a concrete example. Our team and AxiomProver landed on the same natural idea: induct on the largest (or smallest) element of a permutation, cut the rest into two pieces, and reason from there. In plain English this is the kind of argument you can sketch in a couple of paragraphs. It feels inevitable once you see it.
Claim — For $n\ge 3$, we have \[2f(s) =\sum_{k=1}^{n} f(s_1,\ldots,s_{k-2})\cdot f(s_{k+1},\ldots,s_{n-1})\cdot \binom{n-1}{k-1}\cdot \varepsilon(s,k),\] where \[\begin{aligned}\varepsilon(s,k)= \begin{cases} 1, & k=1 \text{ or } k=n \text{ or } s_{k-1}\ne s_k,\\ 0, & \text{else}. \end{cases}\end{aligned}\]
Here we let $f = 1$ in degenerate cases.
Proof: The idea is that given a permutation $(a_1,\ldots,a_n)$ counted by $s$, we could consider slicing it at an index $i$ for which $a_i \in \{1,n\}$. The left-hand side $2f(n)$ counts the number of ways to do so.
For the right-hand side, $\varepsilon(s,k)$ counts whether it’s possible for $1$ or $n$ to be at the index $k$ (at most one of them is possible).
If we perform a slicing like so, the two remaining sequences don’t interact and the number of ways to do so is $\binom{n-1}{k-1}$ for choosing which $k-1$ numbers are to the left of the slice, and which $n-k$ are to the right, times the relevant $f$-terms.
Lean, however, does not get to borrow our human shortcuts. Every little corner case and bookkeeping detail has to be spelled out explicitly. As a result, the current Lean formalization is 2,054 lines long and took 518 minutes to generate! That’s not a knock on Lean; this is just the tax you pay to go from this is the obvious proof to this is a machine-checked proof. And yes, this file isn’t optimized; there’s room to prune it down. But it still illustrates the point: informal clarity and formal verbosity can be very far apart.
Problems that AxiomProver cracked surprisingly while humans didn’t expect it to
There’s Still Hope on Combinatorics, And Geometry Engine Is Not A Must-Have
Combinatorics problems are, historically, not AI’s strong suit. In fact, they were so notorious that many engineering teams more or less wrote them off. Many of the hardest recent IMO problems fall squarely into this category; the lone unsolved problem from IMO 2025, and two from IMO 2024, are combinatorics. Here, at a first glance at A3, we see a combinatorial game theory problem! For B1, Euclidean geometry is its own headache entirely. Doing it properly could require a full geometry engine, which AxiomProver doesn’t have yet.
So we were surprised when the system autonomously solved A3 and B1. The office had screams of excitement; we did not think either of these was within reach!
A3. Alice and Bob play a game with a string of $n$ digits, each of which is restricted to be $0$, $1$, or $2$. Initially all the digits are $0$. A legal move is to add or subtract $1$ from one digit to create a new string that has not appeared before. A player with no legal move loses, and the other player wins. Alice goes first, and the players alternate moves. For each $n\ge 1$, determine which player has a strategy that guarantees winning.
B1. Suppose that each point in the plane is colored either red or green, subject to the following condition: For every three noncollinear points $A$, $B$, $C$ of the same color, the center of the circle passing through $A$, $B$, and $C$ is also this color. Prove that all points of the plane are the same color.
What this seems to suggest is not that geometry or combinatorial game theory are suddenly easy, but rather that the usual pessimism is not universally correct. We would still expect a randomly chosen problem from these areas to be difficult to formalize, and there is clearly a lot of work left to do. Still, these examples show that the barrier is more nuanced than we had assumed.
For A3, we got a bit lucky. The problem does not require exploring the entire game tree. In fact, there is a very clean winning strategy for Bob that can be described succinctly. Once you see it, Bob doesn’t need to respond with much care to Alice’s moves at all. Namely, he just executes the strategy without thinking. This makes the problem much more tractable for Lean as well; there’s little state to track, and no complicated branching to reason about.
Problem B1 is perhaps even more amusing. The statement involves the geometric notion of a circumcenter, and the system produced a solution that was genuinely geometric in flavor. Our mathematicians, upon reading it, found it difficult to follow without a diagram, which is somewhat ironic, since the machine never drew one. In the end, they had to sketch the configuration by hand to understand what was going on:
To give a concrete sense of how these machine proofs line up with human geometric intuition, here is a snippet of Lean code establishing that two circles intersect in exactly two points (in a specific configuration where each circle passes through the other’s center, which is distinct):
For a human reader, the accompanying picture makes the situation immediately clear. The interesting contrast is that the machine seems perfectly content reasoning purely symbolically, while we humans very much want pictures.
For comparison, our group came up with a similar geometric argument involving eight points. It starts with a non-monochromatic equilateral triangle $ABC$, introduces two additional points $X$ and $Y$, and then derives a contradiction using three red points $T_i$ that are equidistant from $A$:
The Problem All Our Mathematicians Tripped On: Victory of Brute Force
We are also honestly shocked that our systems eventually solved A6. This is a problem that defeated basically everyone in-house.
A6. Let $b_0=0$ and, for $n\ge 0$, define $b_{n+1}=2b_n^2+b_n+1$. For each $k\ge 1$, show that $b_{2^{k+1}}-2b_{2^{k}}$ is divisible by $2^{2k+2}$ but not by $2^{2k+3}$.
One of our mathematicians recognized it as living in the world of p-adic arithmetic dynamics (which is a flourishing field at the intersection of arithmetic geometry and number theory: very fun stuff). He knew you needed to be really careful with p-adic power series expansions, and he even had the right idea. But having the right idea and actually finishing the problem are two different beasts, and for A6, our machines won that particular fight.
Our system just did it in 5 hours and the second highest number of tokens among the 12 problems. You can see the Lean code below. The especially amusing part is how it handles differentiation of the relevant power series. It’s doing it in this wonderfully clunky way that no human would ever write, but hey, it works. Sometimes brute force is its own kind of elegance.
Problems where AxiomProver and humans solved via different math approaches
Humans’ Algebraic Instinct Versus AI’s Geometric Method
Problem A4 is probably the most interesting story of the bunch.
A4. Find the minimal value of $k$ such that there exist $k$-by-$k$ real matrices $A_1,\ldots,A_{2025}$ with the property that $A_iA_j = A_jA_i$ if and only if $|i-j| \in \{0,1,2024\}$
What makes this one fun to talk about is that the humans and the AI approached it in genuinely different ways. Most of our mathematicians would instinctively reach for algebra or symbol-pushing. The system, on the other hand, clearly thought geometrically.
Even among the humans, there was some divergence. One pretty quickly found a construction for $k = 2025$ and started suspecting the answer would grow as a function of $n = 2025$ somehow. The other, meanwhile, was building up from small cases. Having easily ruled out $k = 2$, he felt the answer was probably $k = 3$.
Working together, they eventually scraped together several ad-hoc constructions for $n \leq 10$ supporting the latter’s guess, but they didn’t have anything close to a general construction. Both of them had a vague sense that representation theory might be lurking somewhere in the background.
And then the system comes in and suggests: hey, what if each $A_i$ is a rank-one projection onto a fixed unit vector $v_i$?
Once you see this, the problem collapses to showing that there exists a set of $2025$ unit vectors in three-dimensional space, where only consecutive vectors are perpendicular (looping back around), which is a much nicer problem to think about.
The irony is that the formal Lean verification spent most of its lines carefully checking that this circle of $2025$ vectors actually works: see the dominant node in proof below. This is exactly the part that a human mathematician would wave their hands at and call intuitive.
Single-Picture Solution Versus Mechanistic Case Work
B4. For $n\ge 2$, let $A=[a_{i,j}]_{i,j=1}^n$ be an $n$-by-$n$ matrix of nonnegative integers such that $a_{i,j}=0$ when $i+j\le n$; $a_{i+1,j}\in\{a_{i,j},a_{i,j}+1\}$ when $1\le i\le n-1$ and $1\le j\le n$; and $a_{i,j+1}\in\{a_{i,j},a_{i,j}+1\}$ when $1\le i\le n$ and $1\le j\le n-1$. Let $S$ be the sum of the entries of $A$, and let $N$ be the number of nonzero entries of $A$. Prove that \[S\le \frac{(n+2)N}{3}.\]
For B4, one of us found a solution that’s best explained with a picture:
The idea is to exhibit an injection from the special diagonal (the first non-zero diagonal) to entries with value 1. If you stare at the picture, the function definition is pretty clear. You can see why it works. The picture speaks for itself.
The problem is that Lean doesn’t think in pictures. Actually formalizing this would have been painful: you’d have to translate all the geometric intuition into something the proof assistant can digest, and by the time you’re done, you’ve killed whatever elegance the construction had in the first place.
The system, naturally, did not bother with any of this. It produced 1061 lines of Lean code representing what can only be described as a tedious bookkeeping argument, grinding through the combinatorial properties of rows and columns until the result falls out. No pictures, no elegance, just raw case analysis.
What’s kind of neat is that the proof has these four dominant combinatorial lemmas. It is a completely different proof structure from the human one: less aha and more I will simply check everything.
Final Thoughts
So that’s our take on Putnam 2025. Again, all our Lean solutions are available here. This was a ton of fun for the AxiomProver team: there’s something deeply satisfying about watching a system grind through competition math in real time, even when it does things no human would ever think to try.
This points to a question we don’t have good answers to yet: what makes a math problem hard for a machine?
What’s hard for humans and what’s hard for machines are different.
For humans, we have decent intuitions. We know problems with heavy case analysis are tedious to enumerate. We know problems requiring one clever construction can make one stuck forever or shout aha! But for machines, we’re still in the dark. A real theory of machine difficulty—what structural features make problems easy or hard for automated provers – seems like a genuinely interesting research direction.
And exactly because humans and machines excel at and struggle with different things, collaboration makes sense. Right now the workflow is simple: humans pose problems, machines find proofs. But you can imagine something more interactive. Machines sanity-checking human ideas in real time. Humans reviewing machine feedback and steering search toward promising directions. Each side complementing the other.
Axiom is building a world where human intuitions are grounded by machine verification and machine verification in turn inspires human intuitions. The machine grinds the beans; the human tastes the coffee.
In mathematics, we’d like to try this collaboration past competition, in actual research. Olympiad problems are closed: here’s a statement, find a proof. Research isn’t like that. You’re introducing definitions, building theories, and choosing which lens to view the problem through. The search space isn’t "which proof works" but "which abstraction makes the problem dissolve."
It’s Grothendieck’s rising sea, you don’t attack the problem, you raise the water level until it eventually surrounds solid land masses.
Which parts will humans play a role, and which parts will machines learn?
We’re not there yet. But days like this make it feel closer.
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