Proposing and solving olympiad geometry with guided tree search

Mathematics olympiads are prestigious competitions in which both proposing and solving problems are highly honoured. Building artificial intelligence systems capable of addressing these olympiad-level challenges remains an open frontier in automated reasoning, particularly in geometry due to its unique blend of numerical precision and spatial intuition. Here we show that TongGeometry, a neuro-symbolic system using guided tree search, both discovers and proves olympiad-level geometry theorems. Within the same computational budget as existing state-of-the-art systems, TongGeometry establishes a larger repository of geometry theorems: 6.7 billion requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among these, three of TongGeometry’s discoveries were selected for regional mathematical olympiads, appearing in a national team qualifying exam in China and a top civil olympiad in the USA. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry problems in the IMO-AG-30 benchmark, outperforming average top human competitors on this specific dataset. It also surpasses the existing state of the art across a broader spectrum of olympiad-level problems and requires only consumer-grade computing resources. These results demonstrate that TongGeometry operates as both a mathematical discoverer and a solver, becoming an artificial intelligence system to achieve this dual capability. The deployment of a preliminary system based on TongGeometry demonstrates practical applications and opens fresh possibilities for artificial-intelligence-assisted mathematical research and education. TongGeometry both solves and proposes olympiad-level geometry problems. It uses guided tree search to find hard but concise problems, making advanced mathematical reasoning more accessible.