AlphaGeometry solves 25 of 30 olympiad geometry problems without human demonstrations
What was demonstrated
AlphaGeometry pairs a language model, trained from scratch on millions of synthetically generated theorems and proofs, with a symbolic deduction engine. On a test set of 30 recent olympiad-level Euclidean geometry problems it solved 25, compared with 10 for the previous best method. Its proofs are human-readable and were evaluated by human experts.
Why it matters
It shows that synthetic data can stand in for scarce human-written formal proofs in at least one mathematical domain, a bottleneck for automated reasoning systems.
Caveats
- Scope is limited to Euclidean plane geometry; the approach was not shown to transfer to other areas of mathematics.
- The test set is small (30 problems), so the comparison with human medallists is approximate.
- Problems were translated into the system's formal language by people before solving.
Technology profiles
Sources
- peer reviewed paper
Solving olympiad geometry without human demonstrations
Trieu H. Trinh, Yuhuai Wu, Quoc V. Le et al.. Nature, 17 Jan 2024. DOI: 10.1038/s41586-023-06747-5.
Last reviewed 20 Oct 2026.