IMO 2022 Problem 4: Euclidean-geometry translation
Follow the latest progress by email.
Choose B,C,D and E with DE=BC. Let T satisfy TB=TD and TC=TE, and choose A with ∠(BA,BT)=∠(ET,EA). Put P=AB∩CD, Q=AB∩CT, R=AE∩CD and S=AE∩DT. Prove P,Q,R,S 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 specialized task turns two perpendicular-bisector constraints and an angle condition into cyclicity of four intersections.
What counts as progress: A proof of the stated cyclicity preserving the translated construction and its nondegenerate intersections.
How the problem developed
- July 2022 · Contest problem [1]
IMO jury The official contest included this geometry problem; the AlphaGeometry benchmark later used a formal translation of the statement.
- 2025 · Benchmark result [2]
Chervonyi et al. The AlphaGeometry 2 evaluation lists IMO 2022 Problem 4 as solved by the system; this later result does not establish that AlphaGeometry 1 solved the separate IMO-AG-30 translation.
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 2022 official problem archive
- Chervonyi et al., Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
- 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