AlphaGeometry

• 1. Introduction

  ›

  AlphaGeometry solved 25 out of 30 geometry problems from the International Mathematical Olympiad, working under the same time limits given to human competitors. That placed the DeepMind program nearly on par with the average human gold medallist at the competition. The previous benchmark for AI geometry had been held by Wu's method, which managed only 10 correct answers from the same problem set. DeepMind published its findings in the peer-reviewed journal Nature on the 17th of January 2024. MIT Technology Review ran its own coverage the same day. How AlphaGeometry arrives at those proofs depends on a partnership between two very different kinds of reasoning.

  31425

• 2. Symbol and Language

  ›

  The Deductive Database Arithmetic Reasoning is the rule-based symbolic engine at the heart of AlphaGeometry. It builds formal proofs by applying domain-specific rules, the same approach traditional geometry programs have always taken. Traditional programs have no fallback when that approach fails. AlphaGeometry added one: a large language model trained on algorithmically generated geometrical proof data.

  When the symbolic engine exhausts its options without finding a proof, it turns to the language model. The language model responds by proposing a new geometrical construct, which gives the engine a fresh line of deduction to explore.

  Whether this two-part design can carry over to other branches of mathematics remains uncertain. Symbolic engines depend on rules built for specific domains, and producing synthetic training data requires the same domain-specific foundation.

  AlphaGeometry 2 extended that architecture in directions the original program could not reach.

  3152

• 3. AlphaGeometry 2

  ›

  AlphaGeometry 2 was published on the 5th of February 2025, roughly a year after the original program. The new version extended the representation language in two directions. It added support for problems involving the movement of objects, and for problems that include linear equations of angles, ratios, and distances.

  The team targeted IMO geometry questions from 2000 through 2024. With the expanded language, AlphaGeometry 2 covered 88 percent of those questions. The core model is Gemini, finetuned on a dataset of problems and solutions generated in the representation language.

  Gemini drives two distinct functions in the system. It proposes auxiliary constructions, such as new lines and points, to guide the tree search as it explores proof paths. It also handles autoformalization, converting a geometry problem from plain English into a formal statement in the representation language.

  The representation language Gemini operates in will need to extend further to reach full coverage of the IMO geometry archive.

  876