IMO 2019 Problem 2: Euclidean-geometry translation
Follow the latest progress by email.
In triangle ABC, choose A₁ on BC and B₁ on AC, and choose P on AA₁ and Q on BB₁ with PQ parallel to AB. Define P₁ on PB₁ by ∠(P₁P,P₁C)=∠(AB,AC), and Q₁ on QA₁ by ∠(CQ₁,QQ₁)=∠(BC,BA). Prove P,Q,P₁,Q₁ are concyclic.
This page concerns the specialized translated task used in the IMO-AG-30 benchmark. The study’s aggregate result does not establish whether this individual task was solved.
Why it matters and what counts as progress
Why it matters: This benchmark task connects parallel transversals with two directed-angle constructions and a cyclic quadrilateral.
What counts as progress: A cyclicity proof using the specialized translated angles and incidence conditions, rather than assuming the original natural-language problem is identical.
How the problem developed
International Mathematical Olympiad The official archive lists this as IMO 2019 P2; it is one of the contest problems later encoded in the specialized IMO-AG-30 geometry language.
Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong (AlphaGeometry) The Nature paper lists this as one of AlphaGeometry’s five unsolved benchmark statements. Its diagnostic figure shows the symbolic engine could complete a proof when given the ground-truth auxiliary construction by a human, but the autonomous benchmark run did not solve it.
Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang H. Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le, and Thang Luong (AlphaGeometry2) The AlphaGeometry2 paper reports solving all 30 statements in the original IMO-AG-30 benchmark, which includes this formalized target. This is a system result on the benchmark encoding, not an independent review of the original contest wording.
AI contribution
AlphaGeometry solves 25 translated Olympiad geometry problems
AlphaGeometry solved 25/30 specialized IMO-AG-30 classical Euclidean geometry translations using learned auxiliary-point constructions plus a symbolic deduction and algebra engine; the paper does not claim all natural-language IMO geometry conditions are represented.
Sources
- IMO 2019 Problems (official archive)
- Trinh et al., Solving olympiad geometry without human demonstrations
- AlphaGeometry IMO-AG-30 formalized problem set
- Chervonyi et al., Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
- AlphaGeometry2 paper, arXiv record
- Trinh and collaborators: Solving olympiad geometry without human demonstrations
- AlphaGeometry source and proof artifacts
- DeepMind account of computer checking
- Precise translated question and assumptions
- AlphaGeometry study and benchmark results
Website timeline
Publication dates and editorial changes.
AlphaGeometry solves 25 translated Olympiad geometry problems