Primary evidence
- Solving olympiad geometry without human demonstrationsS1 · Primary research · Paper · 2024-01-17
- google-deepmind/alphageometryS1 · Primary research · Repository · 2024-01-17
AlphaGeometry reaches near gold-medallist performance on olympiad geometry benchmark
AlphaGeometry combines a neural language model trained on synthetic theorem/proof data with a symbolic deduction engine. The language model proposes auxiliary constructions and the symbolic engine checks deductions.
What happened?
On IMO-AG-30, a benchmark of 30 translated olympiad-level geometry problems, AlphaGeometry solved 25 problems versus 10 for the previous reported best method, approaching the estimated average performance of an IMO gold medallist on the same set.
Why it matters
It showed that synthetic data plus neuro-symbolic search could overcome a scarcity of human formalized geometry proofs and produce machine-checkable, human-readable olympiad-style solutions.
Significance rationale: AlphaGeometry sharply improved automated performance on a curated olympiad-geometry benchmark and provided a prominent neuro-symbolic example of synthetic-data-driven theorem proving.
Historical context
Earlier developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- AI primary, human verified
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Symbolic, Hybrid
- AI contribution
- The learned model proposed proof-relevant constructions while the symbolic engine performed rule-bound deductions and checked the resulting proof structure.
- Human contribution
- Researchers built the geometry representation, symbolic engines, synthetic-data pipeline, model and evaluation benchmark; human experts also evaluated selected outputs.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- alphageometry
- Organizations
- google-deepmind, new-york-university
- Problems
- imo-ag-30
- Methods
- neuro-symbolic-reasoning, synthetic-data, theorem-proving
Sources & artifacts
- Solving olympiad geometry without human demonstrationsS1 · Primary research · Paper · accessed 2026-09-10
- AlphaGeometry — An Olympiad-level AI system for geometryS2 · Official institutional · Official announcement · accessed 2026-09-10
- google-deepmind/alphageometryS1 · Primary research · Repository · accessed 2026-09-10
- AlphaGeometry source code and model repositoryArtifact · Code
Verification history
- 2024-01-17 · Paper released · E3 · Inspectable artifact
Nature paper, supplementary solutions, source data, and an official code/model release were available.
Corrections
No corrections recorded.