AlphaProof, AlphaGeometry, and the IMO gold: what was actually solved

In July 2025, two AI labs said their models had reached gold-medal level at the International Mathematical Olympiad. The headline version of that story is “AI is now as good at math as the best teenagers in the world.” As a high-school student interested in math and machine learning, I find this milestone unusually close to home.

I wanted to know what was actually solved, by what, under what conditions, and who checked. The answer turns out to be more interesting than the headline. My short version, which I’ll argue for below: the 2025 results are a real jump, bigger than the 2024 ones even though both are called “medal-level,” but “gold medal” is still the wrong unit for measuring whether AI can do mathematics.

January 2024: AlphaGeometry, geometry only

The story starts with a narrow system. On January 17, 2024, Google DeepMind published AlphaGeometry in Nature, in a paper titled “Solving olympiad geometry without human demonstrations.”¹ It only does Euclidean plane geometry, which is the part of olympiad math that looks most like a search problem.

The design is a hybrid. A symbolic deduction engine does the rigorous step-by-step reasoning, the kind of thing a computer has been able to do for decades. A language model, trained from scratch on synthetic data, suggests “auxiliary constructions”: extra points or lines that a human solver would add to a diagram to make the problem crack open. The synthetic data is the clever part. Instead of learning from human proofs, which are rare in machine-checkable form, DeepMind generated about 100 million unique examples of theorems and proofs.²

On a test set of 30 olympiad geometry problems, AlphaGeometry solved 25. The previous best method solved 10, and the blog post says the average human gold medalist solved 25.9 of the same problems.² The paper’s abstract describes this as “approaching the performance of an average International Mathematical Olympiad (IMO) gold medallist.”¹

Two reactions from the announcement stuck with me. Evan Chen, a well-known olympiad coach, said “AlphaGeometry’s output is impressive because it’s both verifiable and clean.”² Fields medalist Ngô Bảo Châu compared geometry problems to chess, since there are relatively few sensible moves at each step.² That comparison is a compliment and a caveat at once. Geometry was picked first because it is the most searchable corner of the competition.

A year later, in February 2025, the team posted AlphaGeometry2. They extended the formal language so it could express more kinds of problems and reported that the system solved 84% of IMO geometry problems from 2000 to 2024, which the paper’s title calls “gold-medalist performance” on geometry.³

July 2024: AlphaProof and a silver, with fine print

At the July 2024 IMO, DeepMind entered two systems after the fact: AlphaGeometry 2 for the geometry problem, and a new system called AlphaProof for everything else.

AlphaProof works in Lean, a programming language for writing proofs that a computer can check line by line. Lean can check a complete proof of the formal statement. Humans still need to check that the statement matches the original problem and uses appropriate assumptions. AlphaProof is trained with reinforcement learning in the style of AlphaZero: it tries to prove statements, Lean tells it whether it succeeded, and it learns from the outcome.⁴ The training set came from automatically translating (DeepMind’s word is “auto-formalizing”) millions of natural-language problems into Lean.

The result was 28 points out of 42, four of six problems solved perfectly. AlphaProof got two algebra problems and one number theory problem, including the hardest problem of the competition, which only five human contestants solved. AlphaGeometry 2 got the geometry problem. Neither system solved either combinatorics problem.⁵ The gold threshold that year was 29, so the combined system landed one point short, at the top of the silver range.⁵

Two mathematicians graded the solutions under the IMO’s normal point rules: Sir Timothy Gowers, a Fields medalist, and Joseph Myers, a two-time IMO gold medalist.⁵ Gowers was impressed by one of AlphaProof’s solutions in particular: “The fact that the program can come up with a non-obvious construction like this is very impressive.”⁵

Now the fine print, which DeepMind stated plainly in its own post.

The problems were translated by hand. People manually rewrote the six problems into formal mathematical language before the systems saw them.⁵ Formalizing an olympiad problem is not trivial. You have to decide exactly what the objects are, and for a “find all functions such that…” problem you have to state the answer in a form Lean can check. That is real mathematical work that humans did.

The time limit didn’t apply. Human contestants get two sessions of 4.5 hours. DeepMind says its systems solved one problem within minutes and took up to three days on others.⁵ When AlphaProof was later published in Nature in November 2025, the abstract described the IMO performance as “achieved with multi-day computation.”⁴ The Nature paper also explains how: for the hardest problems, AlphaProof uses “test-time RL,” generating and learning from millions of related variants of a problem while it is trying to solve it.⁴

It wasn’t an official entry. The grading was done by two very qualified people, but the IMO did not certify the result the way it did in 2025.

None of that makes 2024 fake. A machine-checked proof of the hardest problem at the IMO is a real thing. Those conditions make the score useful as evidence of capability, but unsuitable as a direct comparison with a contestant’s result.

July 2025: two golds, two very different announcements

The 66th IMO was held on the Sunshine Coast in Australia from July 10 to 20, 2025. There were 630 contestants. The gold cutoff was 35 points, and 72 students reached it.⁶ Five students got perfect scores.⁶

Here is the order things happened in, because the order became part of the story.

On July 17, before any lab announced anything, the MathArena team published an evaluation of publicly available models on the 2025 problems. The best was Gemini 2.5 Pro with 13 points out of 42, which they noted was “not enough for a bronze medal (19/42).”⁷ So the starting point for released models was well below the medal range.

On July 19, Alexander Wei of OpenAI posted a thread on X saying that “our latest @OpenAI experimental reasoning LLM” had reached gold-medal-level performance.⁸ According to the thread, OpenAI ran the model on the 2025 problems “under the same rules as human contestants”: two 4.5-hour sessions, “no tools or internet, reading the official problem statements,” and writing natural-language proofs.⁸⁹ Each proof was graded by “three former IMO medalists” who had to agree on the score, and the model got 35 out of 42, solving five of six.⁹ OpenAI posted the proofs to GitHub. The repository has files for Problems 1 through 5 and none for Problem 6.¹⁰ Wei also said, “We don’t plan to release anything with this level of math capability for several months.”⁸

On July 21, Google DeepMind announced that an advanced version of Gemini Deep Think had also scored 35 out of 42, also solving five of six, also in natural language and within the 4.5-hour limit.¹¹ The difference was the grading. DeepMind’s solutions were graded and certified by the IMO’s own coordinators, using the same criteria as for student papers. The post quotes IMO President Gregor Dolinar: “We can confirm that Google DeepMind has reached the much-desired milestone, earning 35 out of a possible 42 points,” and called it a gold medal score.¹¹ He added that the graders found the solutions “clear, precise and most of them easy to follow.”¹¹

Both systems missed Problem 6, the one problem that was much harder than the rest.¹²

The fight over who announced when

The two labs got the same score, and most of the public conversation that week was about something other than math.

DeepMind’s position was that it waited on purpose. Demis Hassabis wrote on X that “we didn’t announce on Friday because we respected the IMO Board’s original request” that labs hold their results until they had been verified and the students had been celebrated.¹³ Thang Luong of Google DeepMind argued that because the IMO has its own private grading guidelines, “any evaluation that’s not based on that guideline could not make any claim about gold-medal level” performance.¹³

OpenAI’s account, as given by Noam Brown and reported by TechCrunch, was different. Brown said the IMO had approached OpenAI months earlier about taking part in a formal contest and OpenAI had declined. After OpenAI learned its score, it contacted the IMO, which asked it to wait until after the Friday night award ceremony, and OpenAI says it did.¹³ The IMO did not respond to TechCrunch’s request for comment.¹³

I can’t settle what was promised to whom, and I don’t think a blog post should pretend to. Here’s what I’m confident of. OpenAI’s result was self-reported and graded by graders it picked. DeepMind’s was graded by the IMO’s coordinators. And even in DeepMind’s case, the IMO only certified the answers. DeepMind’s own post says the IMO’s “review does not extend to validating our system, processes, or underlying model.”¹¹ Nobody outside either company knows how much compute was used, how many attempts were made, or how the final answers were chosen.

That last point is exactly what Terence Tao wrote about on Mastodon on July 19, the same day as OpenAI’s thread.¹⁴ He didn’t single out either lab. Instead, he listed ways a team leader could change the format of the olympiad without technically doing the problems for the students: giving them days instead of hours, rewriting the questions into an easier format, letting six students work together, or submitting only the best of several attempts. Under some of those formats, he wrote, a student who might not reliably get bronze could get gold reliably. His conclusion was that “one should be wary of making overly simplistic apples-to-apples comparisons” between models and human contestants. He also set a personal rule: “I will not be commenting on any self-reported AI competition performance results for which the methodology was not disclosed in advance of the competition.”¹⁴

I think Tao’s thread is the most useful thing anyone wrote that week. It doesn’t say the results are fake. It says that a single score hides several choices, and you can’t judge the score without knowing them.

What the machines did and what people did

Put the three results side by side and track who did each step.

Problem selection was done by humans every time, and this matters more than it sounds. IMO problems are written and chosen by people for a test where high-school students get four and a half hours for three problems.¹⁴ The problems are selected to be approachable with elementary methods in a contest setting, even when very few contestants solve them. The difficulty is curated. A research problem has no such guarantee.

Formalization was done by humans in 2024 and by nobody in 2025. This is the biggest change in the whole timeline. In 2024, the systems were handed a precise, machine-readable statement, and the hard work of “what does this problem actually ask” was already done. In 2025 the models read the same English text the students read.

Solving was done by the machine in all three cases. But “the machine” covers a lot. In 2024 it was a narrow system that searched for days per problem. In 2025 DeepMind says it used “parallel thinking,” exploring many candidate solutions at once before settling on an answer.¹¹ Wei’s thread gave few details about OpenAI’s method.⁸ Neither lab said how much compute went into one run.

Checking flipped direction. In 2024, the Lean proofs were checked by a computer, so correctness wasn’t in doubt; I think the human graders were mostly confirming that the formal statements matched the problems as intended. In 2025 the proofs were in English, so humans had to check them the way they check student papers. That is why the grading dispute mattered so much in 2025 and barely came up in 2024. A natural-language proof is only as trustworthy as whoever read it.

I read through a couple of OpenAI’s posted proofs. They are correct as far as I can follow, and they are also strange to read: terse, full of shorthand, nothing like the polished write-ups in a solutions booklet. That’s not a criticism of the math. It’s a reminder that “graded as correct” and “a proof a human would want to read” are different things, and the grading alone establishes the first, not the second.

Why “gold medal” overstates it

I’ve spent enough time on olympiad-style problems, nowhere near IMO level, to know what kind of thing they are. They are hard puzzles with known answers. That combination is the part the headline drops.

Known answers. Every IMO problem has a solution the committee already knows. The problem is guaranteed to be solvable, guaranteed to fit in a few pages, and designed not to require university-level machinery, though olympiad techniques go well beyond many school syllabuses. Research math has none of those guarantees. Most of the work in research is figuring out which question to ask and whether it’s even true.

A thin slice of difficulty. Greg Burnham at Epoch AI argued in August 2025 that the 2025 paper was unusually lopsided: five problems that weren’t harder than what earlier systems could already handle, and one problem, P6, that was far harder and that no AI solved. His summary: “The problems gave AI only a slim chance to show new capabilities.”¹² Both labs scored exactly 35, which is exactly five perfect solutions and exactly the gold cutoff.⁶ Seventy-two students also reached that line, and five of them got all six.⁶ “Gold” here means “tied with the bottom of the gold range,” not “beat the best humans.”

One test, one sitting. An olympiad is designed to rank teenagers on one weekend. It was never meant to be a benchmark for machines, and it can’t be rerun with fresh problems. Tao’s point applies directly: we don’t know how many attempts went into each answer, or how the final one was chosen.¹⁴

So when someone says “AI won gold at the IMO, so it can do math now,” the honest response is that it can do a specific, curated, well-posed kind of math, with answers that exist, under conditions we can’t fully see.

Why it also understates it

That said, I think a lot of the skeptical reaction went too far in the other direction, and treated 2025 as the same story as 2024 with a bigger number. It wasn’t.

Natural language is a different problem. AlphaProof’s 2024 result required people to translate the questions into Lean first. Both 2025 systems read the problem the way a student does and wrote the proof the way a student does.¹¹⁸ Removing the human translation step removes the part where a mathematician quietly does a chunk of the thinking.

The time limit is a different problem. Three days per problem versus 4.5 hours per three problems is not a small gap.⁵¹¹ Even if the 2025 systems used enormous parallel compute during those hours (and I’d guess they did), they did it in wall-clock time comparable to a student.

General models, not geometry engines. AlphaGeometry was built for one domain. AlphaProof was built for Lean. The 2025 systems were versions of general-purpose language models. DeepMind said a version of its model would go to trusted testers, including mathematicians, before a wider release to Google AI Ultra subscribers.¹¹

The jump from public models was large. Two days before OpenAI’s thread, the best public model scored 13 out of 42 on the same paper, below bronze.⁷ Going from 13 to 35 on a fresh set of problems, with no human translation, is the actual news.

So “gold medal” undersells the change between 2024 and 2025 even as it oversells what a gold medal means about mathematics. Both things are true at once, and I think most of the arguing that week came from people picking one.

What I think it tells us

What gets me is that a system can work through problems like these in ordinary mathematical language. Even with all the limits of the comparison, that opens up a much more interesting question than where it would sit on a medal table: what could someone do with this kind of help while they are still learning, or while they are stuck on a proof?

I wouldn’t take an olympiad result as an answer about research. A competition gives you a carefully chosen problem and a reason to believe there is a solution. Research can leave you wondering whether you asked the right question at all. I’d like to see how these systems handle that uncertainty, including when they should abandon an approach.

The future I’d be excited about is one where a model helps develop an argument that people can check and learn from. Tao’s discussion of AI in mathematics makes the process around a result worth paying attention to as well as the result itself.¹⁴ A score tells us something useful, but seeing how the work happened would tell us much more about what to build next.

Sources