“Solving olympiad geometry without human demonstrations,” by Trieu Trinh, Yuhuai Wu, Quoc Le, He He and Thang Luong of Google DeepMind and New York University, was published in Nature in January 2024. It introduced AlphaGeometry, a system that solves the kind of plane-geometry problems posed at the International Mathematical Olympiad (IMO).
AlphaGeometry is neuro-symbolic: a symbolic deduction engine applies formal geometric rules to derive what follows from a diagram, while a neural language model suggests the clever auxiliary constructions (extra points and lines) that unlock hard problems. Crucially, the system was trained without human-written proofs. The authors generated about a hundred million synthetic theorems and proofs to teach the language model. On a benchmark of 30 olympiad geometry problems from 2000 to 2022 (IMO-AG-30), AlphaGeometry solved 25 within competition time, far ahead of the previous best automated method (which solved 10) and close to the average human gold medalist’s 25.9.
The result was notable because olympiad geometry demands creative problem-solving, not just mechanical calculation, and because the system reached that level by learning from machine-generated data rather than copying human solutions. It became a landmark in the effort to give AI systems rigorous, checkable mathematical reasoning.