AlphaGeometry — An AI That Learned Olympiad Geometry Without Human Examples

AlphaGeometry is an AI system for proving plane-geometry problems, published in Nature on 17 January 2024 by researchers at Google DeepMind and New York University. On a set of 30 geometry problems drawn from the International Mathematical Olympiad (IMO) between 2000 and 2022, called IMO-AG-30, it solved 25 within competition time limits. The previous best method solved 10, and according to DeepMind the average IMO gold medallist solved 25.9. The heart of the work was that it used no human solutions at all: it learned only from 100 million theorems and proofs that the machine synthesised for itself.

After games with AlphaGo (2016) and proteins with AlphaFold (2020), the next arena DeepMind chose was a competition for secondary-school mathematicians.

Why geometry was hard for AI

The paper locates the main obstacle in a shortage of training data. Translating human proofs into a formal language a computer can verify is expensive, and geometry is especially awkward: in a general-purpose proof assistant such as Lean, merely stating most IMO geometry problems still requires a great deal of groundwork. Geometry proof examples were therefore scarce, and existing approaches relied on symbolic methods and human-designed, hard-coded search heuristics.

The best known is Wu's method, which turns a geometric statement into polynomial equations in the coordinates of its points. In principle it can decide every problem in the test set, but it produces no human-readable proof.

Neuro-symbolic: a language model for constructions, an engine for deductions

AlphaGeometry has two parts. One is a symbolic deduction engine, called DD + AR in the paper, that chases angles, ratios and distances to derive new facts. The other is a neural network language model that proposes auxiliary constructions, the extra points and lines a solver adds to a diagram. DeepMind compared the pairing to the idea of thinking fast and slow: one part supplies quick, intuitive ideas and the other does deliberate reasoning.

The training data was home-made. The team sampled nearly a billion random premises, traced what the symbolic engine could derive from each, and extracted 100 million synthetic theorems with proofs, many with more than 200 steps, which the paper notes is four times the average length of olympiad proofs. A Transformer language model was pretrained from scratch on all of it and then fine-tuned on the roughly 9% of proofs that needed auxiliary constructions.

The symbolic engine alone solved 14 problems; the language model's constructions added another 11. The paper reports that even with only 20% of the training data the system solved 21. The hardest problem it failed was IMO 2008 Problem 6, on which human contestants averaged 0.28 points out of 7.

Proofs people can read

AlphaGeometry's proofs are checked by computer and then output in a form people can read. According to the paper, it solved every geometry problem from IMO 2000 and IMO 2015 under human expert evaluation, and for IMO 2004 Problem 1 it found a more general version of the theorem.

Evan Chen, a mathematics coach and former olympiad gold medallist whom DeepMind asked to evaluate a selection of its solutions, said: "AlphaGeometry's output is impressive because it's both verifiable and clean." He also noted that it used classical geometry rules with angles and similar triangles, just as students do, rather than pages of coordinate algebra. The Fields medallist Ngô Bảo Châu added: "But I still find it stunning that they could make it work."

DeepMind released the code and model. It also described AlphaGeometry as the first AI model able to pass the IMO bronze-medal threshold in 2000 and 2015 on the strength of its geometry alone; that is the developer's own claim.

Where was the bar? A rebuttal and a successor

Three months later, in April 2024, Shiven Sinha and colleagues posted a paper on arXiv that questioned the baseline itself. Used well, they reported, Wu's method alone solves 15 of the IMO-AG-30 problems; combined with classic synthetic methods it reaches 21; and combined with AlphaGeometry it reaches 27. The result invited a closer look at how much of the advance came from machine learning and how much from the underlying symbolic machinery.

DeepMind kept improving the system. Its successor, AlphaGeometry2, contributed to silver-medal standard with AlphaProof at IMO 2024, and a February 2025 paper reported that the share of IMO 2000–2024 geometry problems the system could express rose from 66% to 88%, and the share it solved from 54% to 84%.

What changed, and for whom

AlphaGeometry tackled only a slice of the olympiad. DeepMind itself noted that each IMO usually has only two geometry problems among six, so the system could address a third of a contest. Even so, the method of letting a machine generate its own practice material in a field short of human data was what the paper presented as a framework for other mathematical domains facing the same data scarcity.

For people who teach olympiad mathematics, what mattered was that AI output took the form of a proof that can be marked. Chen contrasted it with earlier AI solutions to proof-based competition problems, which he called hit-or-miss. The thread runs on to AlphaProof six months later and to gold-medal-level performance at IMO 2025. The wider picture is on the AI and mathematics timeline and the AI timeline.