Introduction
Lately I have been building products around AI for Math, not the kind of tools that just let a large model explain solutions, but systems more focused on structured geometric expression, constraint relations, diagram structure, and reasoning capability.
As you work on this long enough, one thing becomes obvious: it is not hard to make AI talk about math, but it is very hard to make AI actually do math.
Geometry is especially hard.
I can ask a model to explain why alternate interior angles are equal, but if I ask it to find the key auxiliary line on its own inside a complex diagram, it starts making things up.
When you look back at Google’s path from that angle, you realize they started addressing this systematically much earlier.
AlphaGeometry (AG1) was the first generation.
AlphaGeometry2 (AG2) is the upgraded version.
If you look at the two generations together, they read like a very clear field report on what breaks inside a math AI system.
I wrote this essay because I want to stand on Google’s shoulders and see:
- where they got stuck
- how they solved it
- which parts are engineering problems
- which parts are cognitive misunderstandings
1. First-Generation AlphaGeometry: What Did It Actually Solve?
The core idea behind AG1 was actually pretty pragmatic: do not expect a large model to prove geometry problems by itself. Let the model do the “guessing,” let the symbolic system do the “reasoning,” and let search do the “finding.”
Concretely:
- the LLM proposes auxiliary constructions
- the DDAR symbolic engine handles angle and ratio reasoning
- the search system traverses possible paths
This architecture is highly rational. It admits that language models are not good at rigorous deduction, but they are good at pattern matching and generating constructions that might be useful. The actual proof work is handed over to the symbolic system.
The key component here is the DDAR reasoning engine.
DDAR stands for Deductive Database of Angle and Ratio.
In simple terms, it is a reasoning system specifically designed for geometry.
The system maintains a continuously expanding "database of geometric relations." At the beginning, it only knows some basic facts. For example:
A, B, C are collinear
D lies on AB
Then it keeps applying geometry theorems, such as:
collinear -> angle is 180 degrees
circle -> equal inscribed angles
similar triangles -> ratio relations
Every time it derives a new relation, that relation is added to the database and the system continues reasoning. This process keeps going until it derives the target conclusion.
In other words, what DDAR does is derive every geometric relation that can be derived.
2. Where AG1 Gets Stuck? (I Ran Into These Too)
AG1 is strong, but its limitations are also obvious.
From an engineering perspective, I see three main bottlenecks.
- Its expressive power is too weak
AG1’s geometry language is very restrained. It supports only a limited set of basic relations, such as:
collinear(A,B,C)
parallel(l1,l2)
perpendicular(l1,l2)
concyclic(A,B,C,D)
equal_angle(...)
But many IMO problems actually need you to express distance relations, ratio relations, and numerical angle calculations, and AG1 cannot express those. For example:
AB = CD
AB / CD = EF / GH
∠ABC = 60°
If the language cannot express these things, the system cannot correctly understand the problem.
The expressive space we give AI determines how complex a task it can handle. It is similar to human civilization: when a concept does not exist in the language, it becomes much harder to truly understand it.
AG1 was clearly constrained here because its language was too narrow.
- Search blows up
A geometry proof is fundamentally about finding one correct path inside a huge space of possible constructions.
For example: which auxiliary line should be drawn? Which perpendicular should be constructed? Which points might be concyclic?
AG1 follows a pattern like "try one construction -> run reasoning -> if it fails, switch to another."
The problem is that there are too many possible auxiliary constructions, so the system can easily get trapped in local search.
- The data problem
One of the biggest challenges in math AI is this: there is no large-scale, high-quality dataset.
AG1’s solution was to randomly generate geometric figures, automatically generate theorems, and automatically generate proofs.
But the complexity of the first-generation generated problems was still limited, and that directly affects the model’s construction ability, making it unable to truly solve harder problems.
3. What AlphaGeometry2 Upgraded
Many people assume AG2 improved simply because the Gemini base model got stronger.
That is certainly one factor, but I think the following upgrades matter more.
- Language expansion
AG2 expands the geometry DSL and adds many new predicates. For example:
dist_eq(A,B,C,D) -> AB = CD
ratio_eq(A,B,C,D,E,F) -> AB/CD = EF
angle_compute(...) -> numerical angle relations
After the DSL expansion, the expression coverage of IMO problems rose from 66% to 88%.
In other words, in the previous version the AI often did not fail because it could not solve the problem; it failed because it could not even read the problem properly.
- Search upgraded
AG1 was basically doing single-tree search. AG2 introduces multiple search trees plus shared intermediate conclusions. You can think of it as several problem-solving teams working in parallel.
That significantly raises the probability of finding the key auxiliary line.
- Reasoning engine optimization
DDAR is strengthened in AG2: new reasoning rules, compressed reasoning graphs, and faster inference.
Faster reasoning naturally makes the search space more controllable.
This is not a glamorous innovation, but it matters a lot.
- Double points
AG2 also contains a very interesting geometry trick called double points.
Simply put, the system is allowed to create two "coincident points" during reasoning. For example:
A ≡ A'
That means A and A' are actually the same point, but inside the reasoning system they can participate in different relations. For example:
A lies on line l
A' lies on circle c
Because A = A', the system can eventually derive:
A lies on circle c
This trick can convert many complicated angle problems into concyclicity problems, and concyclicity is easier for the reasoning system to handle.
If you have done olympiad geometry before, this way of thinking will feel familiar. AlphaGeometry2 simply systematizes it.
4. Result Comparison
Looking at the final results, AG2’s improvement is actually very obvious.
In DeepMind’s official report, they evaluated all IMO geometry problems from the past 25 years (2000-2024).
| System | Solve rate |
|---|---|
| AlphaGeometry (AG1) | 54% |
| AlphaGeometry2 (AG2) | 84% |
On the same problem set, AG2 improved solving performance by 30 percentage points.
The DeepMind research team also gave a very interesting comparison:
A score of 42/50 already exceeds the level of an average IMO gold medalist.
Another important metric is problem coverage.
Many geometry problems could not even be represented in AG1, because the language was too narrow.
After AG2 expanded the DSL:
| Metric | AG1 | AG2 |
|---|---|---|
| Expressive coverage of IMO problems | 66% | 88% |
Once the language expands, system capability immediately jumps to another level.
DeepMind also mentioned in its official blog that in the IMO 2024 testing setup, AG2 solved one competition problem in just 19 seconds after formalization, and reached an overall score of 28/42, close to the gold-medal cutoff.
5. Final Thoughts
AlphaGeometry2 proves one thing:
Inside a structured system, AI can become extremely strong.
If you expect a pure LLM to directly prove IMO geometry problems, I do not think that is realistic in the next few years.
But LLM + domain language + symbolic engine + search system is a very robust direction.
Standing on the shoulders of giants for a moment can save a lot of unnecessary detours.
If math AI systems keep evolving over the next few years, my guess is that the keywords will be:
- stronger structure
- better language
- more refined search
That may matter far more than we imagine.