Solving olympiad geometry without human demonstrations

ABSTRACT

Proving mathematical theorems requires deep logical reasoning and intuition, representing a grand challenge for AI. We introduce AlphaGeometry, a neuro-symbolic system that solves complex geometry problems from the International Mathematical Olympiad (IMO) without relying on human demonstrations. AlphaGeometry combines a neural language model, trained on 100 million synthetically generated theorems, with a symbolic deduction engine. When evaluated on 30 IMO geometry problems, AlphaGeometry solved 25, approaching the performance of an IMO gold medalist. This work demonstrates that AI can achieve expert-level mathematical reasoning through synthetic data generation and neuro-symbolic integration.