IMO 2011 Problem 6: Euclidean-geometry translation

Let P lie on the circumcircle of ABC and choose Q on its tangent at P. Reflect both P and Q across each of BC, CA, AB, obtaining three lines through corresponding reflected pairs. Their pairwise intersections form a new triangle with circumcenter O₁; let O be the original circumcenter. Prove a common point X of the two circumcircles is collinear with O and O₁.

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 task concerns a rigid relationship between a reflected tangent construction and the centers of two circles.

What counts as progress: A proof of the center-line conclusion for the translated common-circle intersection, with all three side reflections included.

How the problem developed

  1. 2011 · Contest appearance [1][3]

    International Mathematical Olympiad The official archive lists this as IMO 2011 P6; it is one of the contest problems later encoded in the specialized IMO-AG-30 geometry language.

  2. 17 Jan 2024 · Benchmark result [2][3]

    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.

  3. 5 Feb 2025 · Benchmark result [4][5][3]

    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.

AI involvementAI-centered
ImportanceNotable
Human understandingFull
Reported

Sources

  1. IMO 2011 Problems (official archive)
  2. Trinh et al., Solving olympiad geometry without human demonstrations
  3. AlphaGeometry IMO-AG-30 formalized problem set
  4. Chervonyi et al., Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
  5. AlphaGeometry2 paper, arXiv record
  6. Trinh and collaborators: Solving olympiad geometry without human demonstrations
  7. AlphaGeometry source and proof artifacts
  8. DeepMind account of computer checking
  9. Precise translated question and assumptions
  10. AlphaGeometry study and benchmark results
Website timeline

Publication dates and editorial changes.