
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.
