AlphaGeometry

AlphaGeometry, published in Nature on January 17, 2024, is DeepMind's system for solving olympiad-level Euclidean geometry. It pairs a neural language model — trained from scratch on 100 million synthetically generated theorems and proofs, sidestepping the data bottleneck — with a symbolic deduction engine: when the symbolic engine stalls, the neural half proposes useful auxiliary constructions (new points, lines), and the engine completes the rigorous proof. On 30 IMO geometry problems from 2000–2022 it solved 25 under competition time limits, approaching the average human gold medalist's 25.9 and far ahead of the prior best (Wu's method, 10).

The system produces human-readable, machine-verified proofs and even discovered a more general solution to a 2004 IMO problem that had escaped experts. DeepMind released the complete source code and trained model as open source, and followed it with AlphaGeometry2, which surpassed the average gold medalist across 25 years of IMO geometry.