# Proposing and solving olympiad geometry with guided tree search

arXiv: https://arxiv.org/abs/2412.10673 · HTML: https://mlsanity.com/paper/2412.10673/

## Key facts

- Cited by 19 papers in the map (data through 14 Oct 2026).
- Placed in Spatial and embodied reasoning, one of 17 directions in LLM reasoning.
- Builds on 21 of its 57 references that are in the map.
- First posted on arXiv 14 Dec 2024.

## Placed in

- LLM reasoning / [Spatial and embodied reasoning](https://mlsanity.com/lr/spatial-and-embodied-reasoning/)

## Builds on (most cited first, 21 of 21)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Training Compute-Optimal Large Language Models](https://mlsanity.com/paper/2203.15556/) (2022)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [Prioritized Experience Replay](https://mlsanity.com/paper/1511.05952/) (2015)
- [Solving math word problems with process- and outcome-based feedback](https://mlsanity.com/paper/2211.14275/) (2022)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [TinyGSM: achieving >80% on GSM8k with small language models](https://mlsanity.com/paper/2312.09241/) (2023)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://mlsanity.com/paper/2406.14219/) (2024)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry](https://mlsanity.com/paper/2404.06405/) (2024)
- [Newclid: A User-Friendly Replacement for AlphaGeometry](https://mlsanity.com/paper/2411.11938/) (2024)
- [Training a First-Order Theorem Prover from Synthetic Data](https://mlsanity.com/paper/2103.03798/) (2021)
- [Formalizing IMO Problems and Solutions in Isabelle/HOL](https://mlsanity.com/paper/2010.16015/) (2020)

## Built on by (most cited first, 19 of 19)

- [Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Models](https://mlsanity.com/paper/2503.09567/) (2025)
- [From System 1 to System 2: A Survey of Reasoning Large Language Models](https://mlsanity.com/paper/2502.17419/) (2025)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving](https://mlsanity.com/paper/2504.15780/) (2025)
- [LeanGeo: Formalizing Competitional Geometry problems in Lean](https://mlsanity.com/paper/2508.14644/) (2025)
- [The Need for Verification in AI-Driven Scientific Discovery](https://mlsanity.com/paper/2509.01398/) (2025)
- [A Survey of Deep Learning for Geometry Problem Solving](https://mlsanity.com/paper/2507.11936/) (2025)
- [Heterogeneous Adversarial Play in Interactive Environments](https://mlsanity.com/paper/2510.18407/) (2025)
- [GenesisGeo: Technical Report](https://mlsanity.com/paper/2509.21896/) (2025)
- [Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions](https://mlsanity.com/paper/2512.00097/) (2025)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean](https://mlsanity.com/paper/2607.19374/) (2026)
- [Grounding Before Generalizing: How AI Differs from Humans in Causal Transfer](https://mlsanity.com/paper/2604.24062/) (2026)
- [BiNSGPS: Geometry Problem Solving via Bidirectional Neuro-Symbolic Interaction](https://mlsanity.com/paper/2606.04648/) (2026)
- [MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4](https://mlsanity.com/paper/2608.02295/) (2026)
- [Euclid-Omni : A Unified Neuro-Symbolic Framework for Plane Geometry](https://mlsanity.com/paper/2608.14585/) (2026)
- [Proving olympiad geometry theorems on a superconducting quantum processor](https://mlsanity.com/paper/2609.14533/) (2026)
- [Dense Neuro-Symbolic Reasoning in a Unified Geometry State](https://mlsanity.com/paper/2610.04280/) (2026)

## Abstract (arXiv)

Mathematics olympiads are prestigious competitions, with problem proposing and solving highly honored. Building artificial intelligence that proposes and solves olympiads presents an unresolved challenge in automated theorem discovery and proving, especially in geometry for its combination of numerical and spatial elements. We introduce TongGeometry, a Euclidean geometry system supporting tree-search-based guided problem proposing and solving. The efficient geometry system establishes the most extensive repository of geometry theorems to date: within the same computational budget as the existing state-of-the-art, TongGeometry discovers 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among them, 10 theorems were proposed to regional mathematical olympiads with 3 of TongGeometry's proposals selected in real competitions, earning spots in a national team qualifying exam or a top civil olympiad in China and the US. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry in IMO-AG-30, outperforming gold medalists for the first time. It also surpasses the existing state-of-the-art across a broader spectrum of olympiad-level problems. The full capabilities of the system can be utilized on a consumer-grade machine, making the model more accessible and fostering widespread democratization of its use. By analogy, unlike existing systems that merely solve problems like students, TongGeometry acts like a geometry coach, discovering, presenting, and proving theorems.