AlphaGeometry

AlphaGeometry is a neuro-symbolic artificial intelligence system developed by Google DeepMind that solves competition-level geometry problems at a standard comparable to human Olympiad gold medalists.^[2] The original system was published on January 17, 2024 in the journal Nature under the title "Solving olympiad geometry without human demonstrations," authored by Trieu Trinh, Yuhuai Wu, Quoc Le, He He, and Thang Luong.^[1] AlphaGeometry was the first AI system to approach human expert-level performance on International Mathematical Olympiad (IMO) geometry problems, solving 25 of 30 benchmark problems within the standard time limit, just below the 25.9 average of a human gold medalist and well above the previous automated record of 10.^[1] A substantially upgraded version, AlphaGeometry 2, was deployed in July 2024 for the actual IMO competition, where it solved Problem 4 within 19 seconds and contributed to a silver-medal-level combined score alongside the separate AlphaProof system.^[3]

What is AlphaGeometry?

AlphaGeometry pairs a neural language model with a symbolic deduction engine to prove Euclidean plane geometry theorems. The language model proposes auxiliary constructions (new points, lines, or circles that do not appear in the problem statement), and the symbolic engine then exhaustively derives every fact that logically follows. The two components alternate until a valid, step-by-step proof is found. Critically, the language model was trained from scratch on 100 million synthetically generated theorems and proofs, never on human-written demonstrations.^[1] DeepMind described it as a system that "solves complex geometry problems at a level approaching a human Olympiad gold-medalist."^[2]

Background: mathematical reasoning as an AI challenge

Formal reasoning over geometric figures has challenged computer scientists for decades. While AI systems have performed well at games, protein structure prediction (AlphaFold), and natural language tasks, mathematical reasoning requires a different kind of capability: the system must not only produce an answer but construct a logically valid proof that can be verified step by step.

Geometry competitions such as the International Mathematical Olympiad present particularly hard instances of this challenge. IMO problems are selected to resist standard computational approaches and require non-obvious auxiliary constructions, where a solver must introduce new points, lines, or circles that do not appear in the original problem statement before a proof becomes tractable.^[2] A human mathematician drawing on years of training can recognize which constructions are likely to help; prior automated systems could not.

Earlier automated geometry solvers relied on algebraic approaches such as Wu's method and the Groebner basis method, or on purely deductive systems called synthetic provers. These tools solved some problems efficiently but plateaued well below the difficulty of IMO geometry. The system that held the record before AlphaGeometry solved 10 of the 30 problems in the IMO-AG-30 benchmark; a human gold medalist averaged 25.9 out of 30.^[1]

AlphaGeometry 1 (January 2024)

When was AlphaGeometry released?

AlphaGeometry was announced on January 17, 2024, simultaneously with the publication of the Nature paper.^[2] The core insight behind the system is that the two main obstacles to automated geometry proving, namely the inability to make good auxiliary constructions and the need for human-annotated training data, can both be overcome by generating vast amounts of synthetic geometric data without human input.^[1]

The system solved 25 of 30 problems in the IMO-AG-30 benchmark, placing it between the performance of a human silver medalist (22.9 problems on average) and the average gold medalist (25.9 problems).^[1] The previous automated record was 10 problems.^[1]

How does AlphaGeometry's neuro-symbolic architecture work?

AlphaGeometry combines two components that work in an interleaved loop:

Symbolic deduction engine (DDAR). The symbolic component is an algorithm called the Deductive Database plus Algebraic Rules (DD + AR, abbreviated DDAR) engine. DDAR computes the deduction closure of a geometric configuration: given a set of initial facts about points, lines, circles, and angles, it exhaustively applies a fixed set of inference rules to derive all additional facts that follow logically.^[1] DDAR is complete within its rule set but cannot introduce new geometric objects. When it can derive no further facts, it halts.

Neural language model. When DDAR halts without having reached the proof goal, the neural language model takes over. It reads the current state of the proof attempt (expressed in a formal geometric language) and proposes an auxiliary construction: a new point, line, or circle to add to the figure. Once that construction is added, DDAR resumes. The two components alternate until either a proof is found or a search budget is exhausted.^[1]

The language model is a transformer-based architecture trained entirely on synthetic geometric data. It operates on sequences of symbols in a purpose-built formal language that describes geometric objects and relationships, rather than on natural language or images.^[1]

How was AlphaGeometry trained without human data?

One of the most important contributions of the AlphaGeometry paper is its method for generating training data without any human-annotated proofs.^[1] The process uses synthetic data generation in two stages.

First, the team used highly parallelized computing to generate one billion random geometric configurations. For each configuration, DDAR computed all derivable facts, producing a large set of (premises, conclusions) pairs.^[1] This is "forward generation": derive everything that is true about a randomly sampled figure.

Second, the team ran a traceback procedure. For each conclusion that required no auxiliary construction, the traceback identifies the minimal subset of premises needed to prove it, yielding a clean training example. For conclusions that required an auxiliary construction, the procedure identifies which points in the figure served as constructs and generates the corresponding proof steps.^[1]

This process yielded roughly 100 million unique geometry theorems and their proofs across a wide range of difficulty levels. Nine million of these examples involved auxiliary constructions, which are the hardest cases.^[1] The final training dataset was filtered to remove near-duplicates.

The language model was trained from scratch on this synthetic corpus. It never saw a human-written proof; all of its knowledge of geometric reasoning came from the synthetically generated data.^[1]

Formal geometry language

AlphaGeometry operates in a formal language developed specifically for Euclidean plane geometry. This language can express:

• Point incidence (a point lies on a line or circle)
• Angle and ratio equalities
• Collinearity, concyclicity, and perpendicularity
• Midpoint and bisector relationships

All geometric facts are encoded as symbolic expressions in this language. The language model takes a sequence of such expressions as input and outputs the description of a new geometric object as a token sequence.^[1]

The language was deliberately restricted in scope to make the formal system tractable. One consequence is that the original AlphaGeometry language could only express approximately 66% of IMO geometry problems from 2000 to 2024.^[4] Problems involving geometric inequalities, area calculations, or combinatorial geometry fall outside this scope entirely.

Performance on IMO-AG-30

The 30-problem benchmark (IMO-AG-30) was constructed by selecting all geometry problems from past IMO competitions that could be expressed in the AlphaGeometry formal language.^[1] The benchmark was used to compare AlphaGeometry against prior systems and against human performance levels.

AlphaGeometry produced human-readable proofs for all solved problems. Every solution was checked and verified by computer, and Evan Chen, a math coach and former Olympiad gold medalist, evaluated a selection of the solutions.^[2]

Architecture in detail

The DDAR symbolic engine

DDAR stands for Deductive Database with Algebraic Rules. It maintains a database of known facts about the current geometric configuration and iteratively applies a fixed set of deduction rules until no new facts can be derived (the fixed point of the rule set).^[1] The rules cover standard theorems of Euclidean geometry, angle chasing, ratio chasing, and distance relationships.

DDAR is sound: it only derives facts that are logically entailed by the premises. It is also complete within its rule set, meaning it will eventually derive every fact that follows from the premises using the available rules.^[1] This soundness property is what guarantees that AlphaGeometry's proofs are correct.

The engine handles both numeric and symbolic relationships. Angle chasing, for example, assigns angle labels and tracks equalities symbolically rather than numerically, which allows DDAR to prove angle equalities that hold for general positions of the figure rather than just for a specific diagram.^[1]

The language model as a construction oracle

The neural language model can be understood as a learned heuristic for choosing which auxiliary construction to make at each step. When DDAR stalls, the language model receives a representation of the current proof state and outputs a probability distribution over possible construction tokens. The most likely constructions are tried first.^[1]

During training, the model learned to associate proof states with the kinds of auxiliary constructions that historically led to proofs in the synthetic training data. This is analogous to how a human student learns to recognize patterns: after seeing many cyclic quadrilateral proofs, for example, a student learns that drawing a circle through three specific points is often a productive move.

The language model does not verify whether its proposed constructions are geometrically valid (e.g., whether a claimed intersection actually exists). DDAR handles validation: if the proposed construction is geometrically impossible or does not add any new useful information, DDAR's deduction closure does not grow and the system backtracks.^[1]

Search procedure

AlphaGeometry uses a beam search procedure over proof attempts. At each step, the language model proposes multiple candidate constructions ranked by probability. DDAR is run for each candidate. If any candidate leads to a proof, the search terminates. If not, the search expands the most promising partial proof states in the beam and repeats.^[1]

This approach is analogous to how Monte Carlo Tree Search was used in AlphaGo: the neural model provides fast, heuristic guidance over a large search space that a purely symbolic system could not efficiently navigate.

AlphaGeometry 2 (July 2024)

AlphaGeometry 2 (AG2) was announced publicly on July 25, 2024 alongside AlphaProof, following its deployment at IMO 2024.^[3] A detailed technical paper, "Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2," was published on arXiv in February 2025 (arXiv:2502.03544).^[4]

How does AlphaGeometry 2 differ from AlphaGeometry 1?

AG2 differs from the original system in several important ways:

Language model. The language model in AG2 is based on the Gemini architecture rather than the smaller custom transformer used in AG1. The paper reports models of several sizes, including a 3.3-billion-parameter Gemini model, trained on TPUv4 hardware.^[4]

Training data scale. AG2 was trained on approximately 300 million synthetic theorems, roughly an order of magnitude more than the 100 million used for AG1. The data generation procedure was also improved to produce more diverse and harder examples.^[4]

Expanded formal language. The AG2 language was extended to handle several classes of problems that AG1 could not express:

• Problems with moving constructs (locus theorems)
• Linear equations involving angles, ratios, and distances
• Non-constructive problem statements

These extensions increased the coverage of IMO geometry problems (2000-2024) from 66% to 88%.^[4]

Improved symbolic engine. The DDAR engine was re-engineered for AG2 with a reduced rule set, faster inference, and improved handling of double points (configurations where the same point arises from two different constructions).^[4]

Shared Knowledge Ensemble of Search Trees (SKEST). AG2 introduced a novel search algorithm that runs multiple parallel search trees and shares intermediate results between them. When one search tree discovers a useful auxiliary construction, other trees can benefit from that discovery, which accelerates the overall search.^[4]

Natural language input pipeline. AG2 includes a pipeline using Gemini to translate geometry problems from natural language into the formal AG language, and an automated diagram generation algorithm. This makes the system more practical for end-to-end use without manual formalization.^[4]

Performance on the full IMO geometry corpus

AG2 was evaluated on IMO-AG-50: the 45 IMO geometry problems from 2000 to 2024, translated into 50 AlphaGeometry-language problems (some problems were split in two). It solved 42 of these 50 problems, a success rate of 84%.^[4] AG1 solved 27 of the same 50 problems (54%). The paper puts the average IMO gold medalist at 40.9 of the 50 problems, so AG2 surpassed an average gold medalist on this benchmark.^[4]

IMO 2024 performance

The 2024 International Mathematical Olympiad was held in Bath, United Kingdom in July 2024. After the competition, Google DeepMind tested AlphaProof and AlphaGeometry 2 on the six official 2024 IMO problems.^[3] DeepMind stated that together the two systems "solved four out of six problems from this year's International Mathematical Olympiad (IMO), achieving the same level as a silver medalist in the competition for the first time."^[3]

How did AlphaGeometry 2 solve IMO 2024 Problem 4?

Problem 4 at IMO 2024 was a geometry problem requiring proof that two angles sum to 180 degrees in a specific configuration involving a triangle, its incenter, and several auxiliary points. AG2 solved the problem within 19 seconds after receiving its formalization.^[3]

AG2's solution introduced a point E on the line BI (where I is the incenter) such that the angle AEB equals 90 degrees. This auxiliary construction, which does not appear in the problem statement, creates several pairs of similar triangles (including ABE ~ YBI and ALE ~ IPC) that allow the required angle relationship to be derived.^[4] The solution was awarded full marks (7 out of 7 points) by Joseph Myers, a two-time IMO gold medalist and Chair of the IMO 2024 Problem Selection Committee.^[3]

What score did AlphaProof and AlphaGeometry 2 achieve at IMO 2024?

AlphaProof is a separate DeepMind system that handles non-geometry problems using reinforcement learning over formal proofs in the Lean 4 theorem prover. At IMO 2024, AlphaProof solved Problems 1, 2, and 6 (two algebra problems and a number theory problem). Problem 6 was solved by only five of the approximately 609 human contestants.^[3]

Together, AlphaProof and AlphaGeometry 2 solved 4 of the 6 IMO 2024 problems, accumulating 28 of the possible 42 points.^[3] The gold medal threshold at IMO 2024 was 29 points, reached by 58 of the 609 contestants; the combined AI score of 28 landed exactly one point below that cutoff, at the top of the silver-medal range.^[3] It was the first time an AI reached silver-medal standard at the IMO.^[3]

Problems 3 and 5 were not solved; both were combinatorics problems outside the scope of either system at the time.^[3]

At IMO 2025, an advanced version of Gemini Deep Think reached gold-medal standard (35 of 42 points) working end-to-end in natural language, without the manual formalization that AlphaGeometry and AlphaProof had needed in 2024.^[10] The AG2 paper reports that its fully automated, natural-language version of AG2 was also used at IMO 2025 and solved the geometry problem (Problem 2) in 20 seconds.^[4]

Comparison with Wu's method and other automated solvers

Wu's method, developed by Chinese mathematician Wen-Tsun Wu in the 1970s, reduces geometric theorem proving to polynomial arithmetic using characteristic set decomposition. It is an algebraic approach rather than a synthetic one and can handle a different class of problems than DDAR.

A 2024 paper by Sinha et al. (arXiv:2404.06405) revisited the AlphaGeometry benchmark and found that the original comparison significantly underestimated Wu's method. When run properly with adequate time limits, Wu's method alone solved 15 of the 30 IMO-AG-30 problems, not the 10 reported in the original paper.^[5]

Crucially, Wu's method solved 2 problems that AlphaGeometry failed on, and AlphaGeometry solved problems that Wu's method failed on. The two approaches have complementary strengths. Combining them produced a new state of the art (27/30) that exceeded the average human gold medalist for the first time.^[5]

This finding does not diminish AlphaGeometry's significance but shows that the classical symbolic approaches were stronger than they had been given credit for in the initial publication.

Is AlphaGeometry open source?

At the time of the Nature paper's publication, Google DeepMind released the AlphaGeometry code and model weights as open source.^[2] The primary GitHub repository is google-deepmind/alphageometry and contains:^[7]

• The full DDAR symbolic engine implementation
• Code for the AlphaGeometry language model inference
• Instructions for reproducing the IMO-AG-30 benchmark results

The repository's download script fetches the model checkpoint and vocabulary from a Google Drive folder; an unofficial mirror of those files exists on Hugging Face (Wauplin/alphageometry). The code is licensed under Apache 2.0 and the checkpoints and vocabulary under CC BY 4.0.^[7]

A separate repository, google-deepmind/alphageometry2, was released in May 2025 containing the AlphaGeometry 2 symbolic engine (DDAR) with examples. As of November 2026 the repository still contains only the symbolic engine; the AG2 language model weights have not been publicly released. The AG2 paper was later published in the Journal of Machine Learning Research (vol. 26, 2025).^[8]

What is AlphaGeometry used for?

The primary significance of AlphaGeometry is as a demonstration that neuro-symbolic systems can achieve expert human performance on formal reasoning tasks by training entirely on synthetic data, without access to human demonstrations.^[1]

Automated theorem proving. AlphaGeometry contributed to renewed interest in automated theorem proving (ATP) as a serious AI research direction. Prior ATP systems for geometry were either fast but limited (DDAR, angle chasers) or general but slow (algebraic methods). AlphaGeometry showed that a learned auxiliary construction oracle could break through the ceiling of pure symbolic methods: in the Nature paper, the language model's constructions added 11 solved problems to the 14 solved by the symbolic engine alone.^[1]

Synthetic data for reasoning. The synthetic data generation technique has broader implications. The approach of generating training data by forward sampling (random configurations) and backward filtering (identifying what constructions were needed) is applicable to other formal reasoning domains beyond geometry. It sidesteps the bottleneck of needing human experts to write proofs.

Mathematical research assistance. While AlphaGeometry was designed for competition problems, the same neuro-symbolic architecture could in principle assist research mathematicians working on problems that involve geometric structures. Researchers investigating geometric configurations, new theorems, or extensions of classical results could use such systems to automate search over large spaces of possible constructions.

Education. The system can generate human-readable proofs with explicit construction steps, making it potentially useful as an educational tool for students learning geometry proof techniques. A student could use the system to check their work or to see alternative proof approaches for a given problem.

End-to-end natural language geometry. AlphaGeometry 2's Gemini-based translation pipeline represents a step toward systems that can accept geometry problems stated in plain text (as they would appear in a textbook or competition paper) rather than requiring manual formalization. This is important for practical deployment in educational or research settings.

What are the limitations of AlphaGeometry?

AlphaGeometry has several important limitations that qualify the significance of its performance:

Scope restriction. The original system can only handle problems expressible in its formal language, which covered 66% of IMO geometry problems. AlphaGeometry 2 extended this to 88%, but the remaining 12% (problems involving 3D geometry, inequalities, non-linear equations, or an arbitrary number of points) remain outside its language.^[4]

Formalization bottleneck. For the IMO 2024 evaluation, DeepMind staff manually formalized the problem statements into the AlphaGeometry language. Full automation of the translation from natural language to formal language remained imperfect, with the Gemini-based translation pipeline introduced in AG2 being a partial solution rather than a complete one.^[4]

Proof verbosity. AlphaGeometry's proofs are sometimes more verbose than elegant human proofs. A system that introduces three auxiliary constructions to reach a conclusion that a skilled human might reach in one step is correct but not necessarily illuminating.

No novel mathematics. AlphaGeometry is a theorem prover, not a theorem discoverer. It takes a stated conjecture and attempts to prove it. It does not generate new conjectures or identify interesting structure in a domain unprompted.

Geometry only. Neither AlphaGeometry 1 nor AlphaGeometry 2 handles algebra, number theory, combinatorics, or analysis. These areas require separate systems (such as AlphaProof for formal algebra and number theory).^[3]

Computational cost. The full AG2 system requires substantial computing resources. Some IMO 2024 problems took AlphaProof up to three days of computation; AG2's P4 solution was unusually fast at 19 seconds, but the system may require significant resources for harder cases.^[3]

Reception

The Nature paper received substantial attention from the mathematics and AI research communities. Nature covered the work in a news story by Davide Castelvecchi, "DeepMind AI solves geometry problems at star-student level,"^[11] and in a Nature Podcast episode titled "This AI just figured out geometry: is this a step towards artificial reasoning?"^[6]

The Nature Podcast episode noted that AlphaGeometry did not solve every geometry problem outside the 2000 and 2015 competitions and that its solutions were very long; Thang Luong said the 109-step solution to IMO 2015 Problem 3 had not been optimized for readability.^[6] The subsequent development of AG2 and the IMO 2024 results addressed some of these concerns by expanding the language and improving natural language translation.

The discovery that Wu's method was stronger than reported in the original paper generated some discussion about proper benchmarking methodology. The authors of the follow-up study emphasized that the two approaches are complementary and that combining them yields better results than either alone.^[5]

Continue reading

• AlphaProofAlphaProof is a reinforcement-learning system from Google DeepMind that finds and verifies formal mathematical proofs in the Lean 4 theorem proverMentioned 10 times above
• RReasoning (artificial intelligence)Reasoning in artificial intelligence is the ability of an AI system to draw inferences, solve problems, and make decisions through structured, multi-step thought rather than a single immediate response.Mentioned 8 times above
• Google DeepMindGoogle DeepMind is an artificial intelligence research and model-development organization at Google.Mentioned 4 times above
• AAutomated Theorem ProvingAutomated theorem proving (ATP) is the use of computer programs to find or check mathematical proofs, expressing both the statement and the proof in a formal_logic so that correctness can be decided…Mentioned twice above
• AAlphaFoldAlphaFold is an artificial intelligence system developed by Google DeepMind that predicts the three-dimensional structure of a protein directly from its amino acid sequence.Listed in See also
• Reinforcement learningReinforcement learning (RL) is a branch of machine learning in which an agent learns to make decisions by taking actions in an environment to maximize a cumulative reward signal, discovering good behavior…Listed in See also

More from See also

• Mathematical reasoning in AI
• Neuro-symbolic AI
• Lean (Theorem Prover)
• International Mathematical Olympiad

More to read

• AlphaGeometry 2
• Artificial Intelligence

Topics:AI ModelsAI for ScienceGoogle DeepMindReasoning Models

References

1. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10 ^11 ^12 ^13 ^14 ^15 ^16 ^17 ^18 ^19 ^20 ^21 ^22 ^23 ^24 ^25Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations. *Nature*, 625, 476-482. nature.com/...s41586-023-06747-5
2. ^1 ^2 ^3 ^4 ^5 ^6Google DeepMind. (2024, January 17). AlphaGeometry: An Olympiad-level AI system for geometry. deepmind.google/...ad-level-ai-system-for-geometry
3. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10 ^11 ^12 ^13Google DeepMind. (2024, July 25). AI achieves silver-medal standard solving International Mathematical Olympiad problems. deepmind.google/...-problems-at-silver-medal-level
4. ^1 ^2 ^3 ^4 ^5 ^6 ^7 ^8 ^9 ^10 ^11 ^12 ^13 ^14Chervonyi, Y., Trinh, T. H., et al. (2025). Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2. *arXiv preprint* arXiv:2502.03544. arxiv.org/...2502.03544
5. ^1 ^2 ^3Sinha, S., Prabhu, A., et al. (2024). Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry. *arXiv preprint* arXiv:2404.06405. arxiv.org/...2404.06405
6. ^1 ^2Nature Podcast. (2024, January 17). This AI just figured out geometry: is this a step towards artificial reasoning? *Nature*. nature.com/...d41586-024-00145-1
7. ^1 ^2google-deepmind/alphageometry GitHub repository. github.com/...alphageometry
8. ^google-deepmind/alphageometry2 GitHub repository. github.com/...alphageometry2
9. AlphaGeometry - Wikipedia. en.wikipedia.org/...AlphaGeometry
10. ^Google DeepMind. (2025, July 21). Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad. deepmind.google/...rnational-mathematical-olympiad
11. ^Castelvecchi, D. (2024, January 17). DeepMind AI solves geometry problems at star-student level. *Nature*. nature.com/...d41586-024-00141-5

Show all 11 references