Atlas record: https://www.aitimeline.dev/en/events/evt-0292/
Research · January 17, 2024
AlphaGeometry
A system combining a language model with a symbolic deduction engine solved 25 of the 30 geometry problems from the International Mathematical Olympiad within the competition time limit.
Why it matters
Close to the average gold medallist, and reached without a single human solution in the training data.
The symbolic engine derives consequences from the premises until it stalls; then the language model proposes an auxiliary construction, an extra point or line, and deduction continues. The model was trained on a hundred million synthetic problems the system generated itself, with no human proofs at all. It joins two traditions that had competed for forty years: logical deduction gives a guarantee of correctness, and a trained model gives the guess about where to start.
Event record
- Event date
- January 17, 2024
- Timeline date
- Event date
- Verification
- Sources gathered automatically · September 18, 2026
- Lines
- ID
- evt-0292
Nature paper of 17 January 2024.
Related events
Earlier
- Related AlphaDev 2023
The second system from the same laboratory in a year to search a space of formal steps.
- Related AlphaZero 2017
The same approach of search guided by a trained model, carried from a game into formal mathematics.
- Enables Wu's method: geometry as algebra 1978links to this record
The AlphaGeometry paper names Wu's method as the previous state of the art: it solved 10 of 30 problems, AlphaGeometry 25.
- Enables Gelernter's machine proves geometry theorems 1959links to this record
The AlphaGeometry paper calls auxiliary constructions the longest-standing subject of the field since its inception in 1959, citing Gelernter's papers of 1959 and 1960.
Later