IMO 2008 Problem 1b: Euclidean-geometry translation
Follow the latest progress by email.
Let H be the orthocenter of triangle ABC and D,E,F the side midpoints. The circles centered at D,E,F through H meet BC, CA, AB in A₁,A₂; B₁,B₂; C₁,C₂. Prove C₁,C₂,B₁,A₁ 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: The target connects points from all three midpoint circles, beyond cyclicity of the two-pair companion task.
What counts as progress: A derivation of cyclicity for this particular cross-circle choice of four points.
How the problem developed
International Mathematical Olympiad The original contest statement was IMO 2008 P1. IMO-AG-30 represents that one contest problem with separate formal targets P1a and P1b; this record tracks target P1b, not a separately numbered contest question.
Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong (AlphaGeometry) The Nature paper lists this among the five benchmark statements AlphaGeometry did not solve; this is a result about the formal translation and the system’s search, not a claim that no human solution exists.
Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, and Matthias Bethge (Wu’s method) Reported that Wu’s algebraic method solved this target, one of the two IMO-AG-30 problems among AlphaGeometry’s five failures that Wu’s method handled. The paper illustrates the generated solution; it does not claim an independent human proof audit for this individual result.
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 2008 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
- Sinha et al., Wu’s Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry
- 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