1 of 55

AlphaGeometry:

A Step Toward Automated Math Reasoning

Hoang Huy Nguyen

ISyE Georgia Tech & former Student Researcher at Google DeepMind

2 of 55

Overview of my work

Stochastic Control

Markov chain mixing

[TAC, under review]

Optimal Transport

[JMLR 2024], [AAAI 2024]

AI reasoning

AI for Sciences

AlphaGeometry 2

[JMLR, under review]

[Nature Geoscience 2025]

Foundations

Applied Probability

AI & Deep Learning

Transfer Learning

Stochastic Networks

[SIGMETRICS 2025]

In addition, I would love share a little bit about my other works as well. Besides my work on AI for Math, I also work extensively on Infinite state space Markov chain mixing with applications to Queuing Theory. Moreover, I also work on Optimization algorithms under the stochastic viewpoint, with applications to large scale Optimal Transport problems. I would love to chat further on these directions.
My research spans from theoretical foundations of Markov chains to Applied Probability and using AI & Deep Learning to tackle real world challenge.

In particular, I develop frameworks to analyze the mixing time of infinite state space Markov chains, such as Lyapunov drift or Markov chain curvature. I then use these machinery to analyze practical service systems such as data centers or ride hailing systems.

New AI paradigm: requires high-quality, structured data

3 of 55

Mathematics and AI

4 of 55

Early computers

First analog computer (300 BC)

First abacus (2700 BC)

5 of 55

Four color theorem 1976

The first major computer assisted proof.
1834 minimal configurations that may require more than 4 colors are generated by a computer algorithm.

Appel and Haken

6 of 55

Computer as a collaborator

Doron Zeilberger

Shalosh B. EKHAD

From 1993, they wrote 100 papers together.

7 of 55

Computers as verifiers (Interactive Theorem Provers)

8 of 55

Automated math reasoning

9 of 55

International Mathematical Olympiad (1959 – Present)

Topics

Algebra
Combinatorics
Number Theory
Geometry

One of the most prestigious pre-collegiate math competitions
Elegant, yet difficult problems, require only high school knowledge
AI-IMO challenge: Build the first AI that can win a gold medal

What would it take to build an AI to solve IMO?

Topics

Algebra
Combinatorics
Number Theory
Geometry

10 of 55

About me

3rd prize All-Russia Geometry Olympiad
2nd place in Vietnam
IMO Silver Medal

11 of 55

AlphaGeometry & AlphaGeometry2

A neuro-symbolic system

11

12 of 55

Challenges

Hallucinations

Data scarcity

?

1+1=3

Answer hallucination

Citation hallucination

Lacks high quality, structured data!

Next token predictor

Reward outcome

Mechanism

13 of 55

Challenges

Hallucinations

Data scarcity

?

1+1=3

Answer hallucination

Citation hallucination

Lacks high quality, structured data!

A consistent solver is needed!

14 of 55

Framework

Problem

AlphaGeometry: DDAR

AlphaProof: Lean

Mechanical solver

Provably Correct Solution

15 of 55

Framework

Problem

Generative

Mechanical solver

Solution

AlphaGeometry: LM

AlphaProof: LM + RL

“... a major limitation of automated theorem provers compared to humans – the generation of original mathematical terms – might be addressable via generation from language models…” Polu & Sutskever, 2020

�

Consistent rewards

Allows self-improvement!

AlphaGeometry: DDAR

AlphaProof: Lean

Simplify

problem

Provide

feedbacks

16 of 55

Example: Solving an equation

Symbolic engine

17 of 55

Outline

AlphaGeometry as a neuro-symbolic solver

How to perform “magical” constructions

Overall architecture

Training data

Language model

Symbolic engine

?

1+1=3

18 of 55

Idea #1: AlphaGeometry is a neuro-symbolic solver

18

19 of 55

Symbolic Engine

19

Not use:

Advanced Theorems
Coordinates
Transformations

The symbolic engine translates our problem into a specific language, which encodes the geometric premises using a very small vocabulary. This language was first proposed by Chou, Gao, Zhang
The symbolic engine then uses these premises to make deductions, which forms the deductive aspect of the engine
In geometry, we also need to establish algebraic relations between sidelengths and angles, and so we have an algebraic component as well. We cast these angles and sidelengths into a system of equations and then use linear algebra techniques to solve them.
With that, we combine deductive and algebraic reasoning to obtain DDAR, and as you can see, it only uses simple stuff
Simple Gaussian elimination-based algorithm
Only uses simple Geometry techniques such as angle chasing, length chasing, ratio chasing
Use simple theorems => long proofs but fast and scalable�
Despite various claims, this component alone is very weak and cannot solve very simple theorems

20 of 55

Idea #1: AlphaGeometry is a neuro-symbolic solver

20

21 of 55

Idea #1: AlphaGeometry is a neuro-symbolic solver

21

Magic Construction

22 of 55

Idea #1: AlphaGeometry is a neuro-symbolic solver

22

System 1 (neural LM, creative) &

System 2 (symbolic engine, reliable).

Explorer

Exploiter

23 of 55

Outline

AlphaGeometry as a neuro-symbolic solver

How to make key constructions

Overall architecture

Training data

Language model

Symbolic engine

?

1+1=3

24 of 55

Idea #2: Synthetic Data Generation at Scale

24

Knowledge-building process similar to humans.

Synthetic data is artificially generated data to emulate the knowledge building process.

For example, imagine Professor Sajad wants to train his PhD students to do research.

The lack of training data for maths, especially those at the Olympiad level, motivated us to generate everything synthetically.

This actually emulate the knowledge-building process similar to humans. For example, if my advisor wants me to do research in applied probability, he will give me lots of simple exercises in stochastic process so that I can notice patterns and gain intuition about the area, which I then use to solve harder research problems that could be out of the training data distribution.

Humans can learn geometry using a pen and paper, examining diagrams and using existing knowledge to uncover new, more sophisticated geometric properties and relationships. Our synthetic data generation approach emulates this knowledge-building process at scale, allowing us to train AlphaGeometry from scratch, without any human demonstrations.

25 of 55

Overview of the data generation process

Solves data scarcity w/o human intervention!

(to find the minimal problem)

Masking

26 of 55

AB=AC DB=DC sameLine(D,B,C)

∠ABD=∠DCA

∠ABC=∠BCA

“Theorem: △ ABC has AB=AC and D the midpoint of BC. Prove ∠B=∠C. Proof: ...”

Unnecessary for theorem Necessary for proof

Identify key constructions

27 of 55

AB=AC DB=DC sameLine(D,B,C)

ABD=DCA

∠ABC=∠BCA

Build tree

Identify key constructions

28 of 55

AB=AC DB=DC sameLine(D,B,C)

ABD=DCA

∠ABC=∠BCA

Build tree
Conclusion traceback → D_C

D_C

Identify key constructions

29 of 55

AB=AC DB=DC sameLine(D,B,C)

ABD=DCA

∠ABC=∠BCA

Build tree
Conclusion traceback → D_C
Object traceback → D_O

D_C

D_O

Identify key constructions

30 of 55

AB=AC DB=DC sameLine(D,B,C)

ABD=DCA

∠ABC=∠BCA

Build tree
Conclusion traceback → D_C
Object traceback → D_O
Dependency difference = D_C\ D_O

D_C

D_O

Identify key constructions

31 of 55

The Final Data

31

32 of 55

32

AG2

50%

Longest IMO AG 2 proof

Proof length = 700+!

AG1

1B random diagram

100M synthetic problems

dedup

33 of 55

The Model

33

34 of 55

By the way, it’s not LLM

151M params (for reference: Llama 3.1 has 405 billions, DeepSeek has 671 billions!)
Transformers: 12 layers, 8 heads, 1K emb dim, 4K hidden dim.
Vocab: 757.
Max context length: 1K. 90% data < 200.
TPUv3 4x4.
Pretraining: 10M steps. Finetuning: 1M steps.

34

35 of 55

The Results

35

36 of 55

37 of 55

All-time IMO Geometry results (2000-2024)

Faster symbolic engine

Knowledge sharing

Better search algorithm

Autoformalization

AG 1

AG 2

38 of 55

Co-author vs AG: IMO 2015 P3

Hoang: 45 minutes

AG 2: 20 minutes

39 of 55

Silver medalist performance at IMO 2024!

AlphaGeometry 2 + AlphaProof

39

40 of 55

AlphaGeometry 2 solved an IMO geometry problem in 19s!

Asymmetric construction
Connect incenter I and midpoints K, L

Human: Trigometry, complex numbers
AG 2: Similar triangles and angle chasing

41 of 55

Takeaway

Hallucinations

Data scarcity

?

1+1=3

Symbolic engines

Language models

Synthetic data generation

LLM for Math Research

42 of 55

Thank you for listening!

Stochastic Control

Markov chain mixing

[TAC, under review]

Optimal Transport

[JMLR 2024], [AAAI 2024]

AI reasoning

AI for Sciences

AlphaGeometry 2

[JMLR, under review]

[Nature Geoscience 2025]

Foundations

Applied Probability

AI & Deep Learning

Transfer Learning

Stochastic Networks

[SIGMETRICS 2025]

In addition, I would love share a little bit about my other works as well. Besides my work on AI for Math, I also work extensively on Infinite state space Markov chain mixing with applications to Queuing Theory. Moreover, I also work on Optimization algorithms under the stochastic viewpoint, with applications to large scale Optimal Transport problems. I would love to chat further on these directions.
My research spans from theoretical foundations of Markov chains to Applied Probability and using AI & Deep Learning to tackle real world challenge.

In particular, I develop frameworks to analyze the mixing time of infinite state space Markov chains, such as Lyapunov drift or Markov chain curvature. I then use these machinery to analyze practical service systems such as data centers or ride hailing systems.

New AI paradigm: requires high-quality, structured data

43 of 55

Thank you!

43

Bonus slides coming up

44 of 55

All-time IMO Geometry results

45 of 55

IMOSL 30 benchmark

46 of 55

IMO 2013 P3

47 of 55

IMO 2014 P3

48 of 55

IMO Shortlist 2009 G7

49 of 55

IMO Shortlist 2009 G7

50 of 55

Some details of AlphaGeometry 2

IMO solving rate: 54% → 84%
An order of magnitude more synthetic data
Handle much more challenging geometry problems

Movements of objects
Equations of angles, ratio or distances.

Can solve IMO 1979, P3!

51 of 55

Knowledge sharing system

52 of 55

Data generation

53 of 55

Data generation

54 of 55

Learning curves

55 of 55

Temperature and number of token seen