What was already known
On the same 30 translated problems, the paper reports that Wu's method, the previous external state of the art, solved 10; the authors' deduction-plus-algebra engine without learned auxiliary constructions solved 14, and their strongest human-heuristic variant solved 18. Generating auxiliary points had long been a bottleneck for synthetic geometry provers.
AI involvement
Human researchers designed the AlphaGeometry architecture and benchmark. The trained language model learned and proposed retained auxiliary-point constructions that the human-designed symbolic engine could not search exhaustively; the paper's ablation attributes 11 additional solved tasks to this component.
Humans designed the benchmark, synthetic data and symbolic engine. The trained language model proposed retained auxiliary constructions, and ablation attributes 11 solved cases beyond the authors’ DD+AR engine to this learned component.
Importance
This was a clear advance in automated Olympiad-style Euclidean geometry on a fixed translated benchmark, raising solved cases from 10 with the previous external method to 25 and showing that learned auxiliary constructions added 11 cases to the authors' own symbolic engine.
Limitations
The benchmark is 30 translated classical-geometry problems, representing about 75% of eligible non-combinatorial geometry tasks; geometric inequalities and combinatorial geometry are outside the language. Solving a translated statement may omit conditions from the original natural-language problem, as the paper's IMO 2004 P1 example illustrates. The model supplied auxiliary constructions while human researchers designed the language, synthetic training data, symbolic engine and evaluation. Later systems may surpass this historical benchmark.
Technical verification
The authors report complete computer verification of each produced solution in their specialized geometry language. This covers 25 translated benchmark statements; the original natural-language problem may include conditions not represented in translation. AIProofWatch did not rerun the engine.
Formal checking
DeepMind states every Olympiad solution produced by AlphaGeometry was checked and verified by computer; the checked objects are the specialized translated geometry statements, not all original-language conditions.
- Checker
- AlphaGeometry symbolic deduction and algebra engine, reported by DeepMind
- Scope
- Machine-checkable proofs of 25 specialized translated IMO-AG-30 geometry statements
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The human authors explain the auxiliary-construction mechanism and analyze representative proofs, failures and translation limits. This supports understanding of the selected benchmark advance, though it is not a human check of all 25 proofs.
Correction and publication history
Primary paper and checking-scope review for the translated IMO geometry benchmark.
Read this published revision