AlphaGeometry: solving olympiad geometry without human demonstrations

A neuro-symbolic theorem prover for Euclidean plane geometry that sidesteps the shortage of human training data by synthesizing millions of theorems and proofs. On a test set of 30 latest olympiad-level problems the authors report it solves 25, versus 10 for the previous best method.

L3Multi-step tool-using agentic workflow Source Peer-reviewed source Outcome Machine-verified artifacts

Evidence & verification

Source level

Peer-reviewed source
Grounded in a peer-reviewed publication. This describes the source; it does not mean the reported results have been independently reproduced.

Outcome verification

Machine-verified artifacts
Key artifacts (for example, formal proofs) were checked mechanically by a proof checker. Higher-level performance claims remain author-reported.

Sources checked

2026-10-15 (UTC)

Peer-reviewed in Nature (Trinh et al., published online 2024-01-17, DOI 10.1038/s41586-023-06747-5, resolved 2026-10-15). Proofs produced by the system are constructed through a symbolic deduction engine, so individual proof steps are formally checkable; the benchmark score (25 of 30) remains the authors' reported evaluation.

Source-checked does not mean independently reproduced. See the Method page for how these labels are assigned.

Sources (2)

Workflow & human oversight

Neural proposals guide a symbolic deduction tool through multi-step proof search. Humans supply formalized problems and assess applicability; this is bounded theorem proving, not an autonomous research programme.

Workflow level is not an evidence score; higher is not better evidence.

Problem

Most machine-learning theorem provers depend on human proofs translated into machine-verifiable form; for geometry, translation is especially hard and training data scarce. The authors ask whether a prover can be trained without any human demonstrations.

Approach

AlphaGeometry pairs a neural language model trained from scratch on large-scale synthetic data with a symbolic deduction engine. The language model guides the symbolic engine through the branching points of challenging problems; the system outputs human-readable proofs.

Outcomes (as reported by the originating team)

The authors report solving 25 of 30 latest olympiad-level problems, outperforming the previous best method (10) and approaching an average IMO gold medallist; solutions to all geometry problems in IMO 2000 and 2015 under human expert evaluation; and a generalized version of a translated IMO 2004 theorem (Trinh et al., Nature, 2024).

Limitations

Scope is Euclidean plane geometry; problems must be encoded into the system's formal language. The 25/30 result is an author-reported evaluation on one curated test set. Not independently reproduced.

Reproducibility

The authors publish code and the synthetic-data generation pipeline at the linked repository (link verified live 2026-10-15), alongside the benchmark descriptions in the publication.

Adoption requirements

Familiarity with formal geometry languages and the system's input format; compute for running the neural guidance model; suitable mainly for research groups studying automated reasoning rather than general mathematics workflows.

Comments

No comments yet.

Add a comment

Comments are held for moderation before appearing. Critical or corrective comments are welcome — especially evidence that an entry overstates what has been verified.