AI Proof WatchKeep up with AI contributions

Synthetic proofs for Olympiad geometry

Individual problem

The IMO-AG-30 benchmark translates 30 International Mathematical Olympiad classical geometry problems into a specialized symbolic language.

Curated contributions 1

Understand the problem ↓

AlphaGeometry solves 25 translated Olympiad geometry problems

  • Mathematics
  • Theoretical Computer Science

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
Technical verificationFormal (AlphaGeometry DD+AR symbolic geometry engine)
Human understandingFull

Understanding the problem

Read the background

The IMO-AG-30 benchmark translates 30 International Mathematical Olympiad classical geometry problems into a specialized symbolic language. The task is to produce valid proofs, often by finding auxiliary points absent from the statement.

Why it matters

Auxiliary constructions were a major bottleneck for geometry theorem provers; learned proposals let a symbolic engine prove many more benchmark problems.

What counts as progress

How many of the 30 translated classical geometry problems can an automated system solve with machine-checkable proofs?

Website timeline

Publication dates and editorial changes.