---
title: "Solving olympiad geometry without human demonstrations"
authors:
  - "Trieu H. Trinh"
  - "Yuhuai Wu"
  - "Quoc V. Le"
  - "He He"
  - "Thang Luong"
year: 2024
venue: "Nature"
arxiv: "2312.12272"
doi: "10.1038/s41586-023-06747-5"
source: "https://arxiv.org/abs/2312.12272"
topics:
  - "mathematical-reasoning"
  - "theorem-proving"
  - "imo"
seed_rank: 1221
seed_batch: "alpoge-math-2026-08-24"
reviewed: "2026-08-24"
pool: "agents"
relevance_score: 10
lineage: ai-mathematical-reasoning
cites:
  []
see:
  []
---

# Solving olympiad geometry without human demonstrations

## One-sentence takeaway

AlphaGeometry: 100M synthetic theorems train a language model to propose auxiliary constructions for a symbolic DD+AR engine — 25/30 recent IMO geometry problems, near average gold.

## Why it matters here

The 2024 Nature event: olympiad geometry without human proofs. Neuro-symbolic, not a MATH increment.

## Problem

Geometry has almost no formal training data; translation into a machine language is itself the bottleneck.

## Design

Synthesize theorems and proofs across difficulty; LM proposes auxiliaries; deduction engine closes. Human-readable proofs.

## Evidence

Nature 625, 476-482 (2024). DOI 10.1038/s41586-023-06747-5. arXiv:2312.12272. 25/30 vs previous 10; IMO 2000 and 2015 geometry all solved under expert eval.

## Limitations

Plane geometry only; specialised language. Silver 2024 needed AlphaProof for the rest.

## Implications for Broadside

See 1222 (AG2) and 1223 (AlphaProof). Do not remint the blog.

## Bottom line

Mint the Nature paper.

## Links

- arXiv: [2312.12272](https://arxiv.org/abs/2312.12272)
- DOI: [10.1038/s41586-023-06747-5](https://doi.org/10.1038/s41586-023-06747-5)