---
title: "Proposing and solving olympiad geometry with guided tree search"
description: "The authors present TongGeometry, a synthetic system for planar Euclidean geometry built around a… 18 references, cited by 7 papers here."
authors: ["Chi Zhang", "Jiajun Song", "Siyu Li", "Yitao Liang", "Yuxi Ma", "Wei Wang", "Yixin Zhu", "Song-Chun Zhu"]
year: 2024
venue: "arXiv:2412.10673"
source: "https://arxiv.org/abs/2412.10673"
doi: "10.48550/arxiv.2412.10673"
arxiv: "2412.10673"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/zhang-2024-proposing-solving-olympiad-geometry-guided/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/zhang-2024-proposing-solving-olympiad-geometry-guided/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2024](https://md.research.elamur.ai/free/en/papers/2024/page/14/) / Proposing and solving olympiad geometry with guided tree search

# Proposing and solving olympiad geometry with guided tree search

**Authors:** [Chi Zhang](https://md.research.elamur.ai/free/en/authors/chi-zhang/), Jiajun Song, Siyu Li, [Yitao Liang](https://md.research.elamur.ai/free/en/authors/yitao-liang/), [Yuxi Ma](https://md.research.elamur.ai/free/en/authors/yuxi-ma/), [Wei Wang](https://md.research.elamur.ai/free/en/authors/wei-wang/), [Yixin Zhu](https://md.research.elamur.ai/free/en/authors/yixin-zhu/) and [Song-Chun Zhu](https://md.research.elamur.ai/free/en/authors/song-chun-zhu/) · **Year:** 2024 · **Venue:** arXiv:2412.10673 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2412.10673) · [PDF](https://arxiv.org/pdf/2412.10673v1) · [DOI 10.48550/arxiv.2412.10673](https://doi.org/10.48550/arxiv.2412.10673) · [arXiv 2412.10673](https://arxiv.org/abs/2412.10673) · [OpenAlex](https://openalex.org/W4405468478)

**Citations:** 1 citations (OpenAlex, 2026-10-14) · [7](https://md.research.elamur.ai/free/en/papers/zhang-2024-proposing-solving-olympiad-geometry-guided/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Automatically creating and proving olympiad-level geometry problems is hard. Geometry mixes numeric and spatial reasoning, the search space branches enormously, and few past problems exist to learn heuristics from. The authors present TongGeometry, a synthetic system for planar Euclidean geometry built around a finite search tree. It generates problems by tracing backward from discovered facts and proves them by forward chaining with a redesigned deductive database (DD) engine.

The search was steered by statistics from 196 olympiad problems and ran massively in parallel. It produced billions of readable problems whose proofs need auxiliary constructions. That data was then used to fine-tune two LLMs: one proposes which construction to try next, and the other estimates how many steps remain.

The guided system proves every problem in IMO-AG-30 on a single consumer workstation, which the authors present as the first result beating an average IMO gold medalist. It also beats AlphaGeometry on a broader olympiad set. Several of its generated problems were accepted by real competitions. The work matters because it covers both proposing and solving at olympiad level while needing only modest hardware.

## Key points
- **Data generation:** The search ran for 30 days on 10,368 CPU cores. It yielded about 6.7 billion problems requiring auxiliary constructions, about 4.1 billion of which have geometric symmetry.
- **Competition use:** Of 10 proposals sent to competitions, 3 were used. One was selected as the sole geometry question at the Beijing round of the 2024 national high school math league, and two were shortlisted for the 2024 US Ersatz Math Olympiad.
- **IMO-AG-30 results:** All 30 problems were solved, each in under 38 minutes, on 32 CPU cores and one NVIDIA RTX 4090.
  - The DD backend alone solved 18 problems.
  - The value model was decisive for IMO 2000 P6 and IMO 2008 P6.
  - For comparison, AlphaGeometry needed 246 CPU cores and 4 V100 GPUs.
- **MO-TG-225 results:** On this new benchmark of olympiad problems, TongGeometry solved 81.3% of problems versus 45.3% for AlphaGeometry. GPT-4 and o1 were also evaluated and frequently produced flawed proofs.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Peking University](https://md.research.elamur.ai/free/en/universities/peking-university/) — University, Beijing, China · 335 works · 43,758 citations
- [Beijing Institute for General Artificial Intelligence](https://md.research.elamur.ai/free/en/government/beijing-institute-for-general-artificial-intelligence/) — Government body, Beijing, China · 14 works · 692 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [➗ Mathematics](https://md.research.elamur.ai/free/en/shelves/mathematics/) · 233 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works · [➗ Geometry and Topology](https://md.research.elamur.ai/free/en/shelves/mathematics/geometry-and-topology/) · 9 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu and Song-Chun Zhu. 2024. Proposing and solving olympiad geometry with guided tree search. arXiv:2412.10673.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{zhang2024proposing,
  title = {{Proposing and solving olympiad geometry with guided tree search}},
  author = {Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu and Song-Chun Zhu},
  year = {2024},
  doi = {10.48550/arxiv.2412.10673},
  eprint = {2412.10673},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2412.10673}
}
```

- [← previous PanGu-π Pro:Rethinking Optimization and Architecture for Tiny Language Models](https://md.research.elamur.ai/free/en/papers/tang-2024-pangu-pi-pro-rethinking/)
- [next → Qabas: An Open-Source Arabic Lexicographic Database](https://md.research.elamur.ai/free/en/papers/jarrar-2024-qabas-open-source-arabic-lexicographic/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/14/)

## References

18 references, 8 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. D. Selsam, et al., IMO Grand Challenge. URL [https://imo-grand-challenge.github.io](https://imo-grand-challenge.github.io) (2020). [↗](https://imo-grand-challenge.github.io)
2. T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong, [Solving olympiad geometry without human demonstrations](https://md.research.elamur.ai/free/en/papers/trinh-2024-solving-olympiad-geometry-without-human/). Nature 625 (7995), 476–482 (2024).
3. S. Polu, I. Sutskever, [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/). arXiv preprint arXiv:2009.03393 (2020).
4. K. Zheng, J. M. Han, S. Polu, [Minif2f: a cross-system benchmark for formal olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). arXiv preprint arXiv:2109.00110 (2021).
5. S. Polu, et al., [Formal mathematics statement curriculum learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). arXiv preprint arXiv:2202.01344 (2022).
6. G. Lample, et al., [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). Advances in neural information processing systems 35, 26337–26349 (2022).
7. J. Achiam, et al., [Gpt-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-gpt-4-technical-report/). arXiv preprint arXiv:2303.08774 (2023).
8. H. Touvron, et al., [Llama: Open and efficient foundation language models](https://md.research.elamur.ai/free/en/papers/touvron-2023-llama-open-efficient-foundation-language/). arXiv preprint arXiv:2302.13971 (2023).
9. W. W. R. Ball, A short account of the history of mathematics (Courier Corporation) (1960). [find](https://scholar.google.com/scholar?q=W%2E+W%2E+R%2E+Ball%2C+A+short+account+of+the+history+of+mathematics+%28Courier+Corporation%29+%281960%29%2E)
10. F. Marić, et al., Formalizing IMO problems and solutions in Isabelle/HOL. arXiv preprint arXiv:2010.16015 (2020). — [arXiv:2010.16015](https://arxiv.org/abs/2010.16015) [find](https://scholar.google.com/scholar?q=F%2E+Maric%CC%81%2C+et+al%2E%2C+Formalizing+IMO+problems+and+solutions+in+Isabelle%2FHOL%2E+arXiv+preprint+arXiv%3A2010%2E16015+%282020%29%2E+%E2%80%94+%5BarXiv%3A2010%2E16015%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2010%2E16015%29)
11. L. d. Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28 (Springer) (2021), pp. 625–635. [find](https://scholar.google.com/scholar?q=L%2E+d%2E+Moura%2C+S%2E+Ullrich%2C+The+Lean+4+theorem+prover+and+programming+language%2C+in+Automated+Deduction%E2%80%93CADE+28%3A+28th+International+Conference+on+Automated+Deduction%2C+Virtual+Event%2C+July+12%E2%80%9315%2C+2021%2C+Proc)
12. S.-C. Chou, X.-S. Gao, J.-Z. Zhang, An introduction to geometry expert, in Automated Deduction—Cade-13: 13th International Conference on Automated Deduction New Brunswick, NJ, USA, July 30–August 3, 1996 Proceedings 13 (Springer) (1996), pp. 235–239. [find](https://scholar.google.com/scholar?q=S%2E%2DC%2E+Chou%2C+X%2E%2DS%2E+Gao%2C+J%2E%2DZ%2E+Zhang%2C+An+introduction+to+geometry+expert%2C+in+Automated+Deduction%E2%80%94Cade%2D13%3A+13th+International+Conference+on+Automated+Deduction+New+Brunswick%2C+NJ%2C+USA%2C+July+30%E2%80%93August+3%2C+1)
13. C. Sangwin, A brief review of GeoGebra: dynamic mathematics. MSor Connections 7 (2), 36 (2007). [find](https://scholar.google.com/scholar?q=C%2E+Sangwin%2C+A+brief+review+of+GeoGebra%3A+dynamic+mathematics%2E+MSor+Connections+7+%282%29%2C+36+%282007%29%2E)
14. P. Bak, R. S. Krajči, M. M. Rolı́nek, Automated generation of planar geometry Olympiad problems, Ph.D. thesis, Master Thesis (2020). [find](https://scholar.google.com/scholar?q=P%2E+Bak%2C+R%2E+S%2E+Krajc%CC%8Ci%2C+M%2E+M%2E+Rol%C4%B1%CC%81nek%2C+Automated+generation+of+planar+geometry+Olympiad+problems%2C+Ph%2ED%2E+thesis%2C+Master+Thesis+%282020%29%2E)
15. D. Guo, et al., DeepSeek-Coder: When the Large Language Model Meets Programming–The Rise of Code Intelligence. arXiv preprint arXiv:2401.14196 (2024). [find](https://scholar.google.com/scholar?q=D%2E+Guo%2C+et+al%2E%2C+DeepSeek%2DCoder%3A+When+the+Large+Language+Model+Meets+Programming%E2%80%93The+Rise+of+Code+Intelligence%2E+arXiv+preprint+arXiv%3A2401%2E14196+%282024%29%2E)
16. J. Hoffmann, et al., [Training compute-optimal large language models](https://md.research.elamur.ai/free/en/papers/hoffmann-2022-training-compute-optimal-large-language/). arXiv preprint arXiv:2203.15556 (2022).
17. J. S. Mackay, History of the Nine-point Circle. Proceedings of the Edinburgh Mathematical Society 11, 19–57 (1892). [find](https://scholar.google.com/scholar?q=J%2E+S%2E+Mackay%2C+History+of+the+Nine%2Dpoint+Circle%2E+Proceedings+of+the+Edinburgh+Mathematical+Society+11%2C+19%E2%80%9357+%281892%29%2E)
18. E. Chen, Euclidean geometry in mathematical olympiads, vol. 27 (American Mathematical Soc.) (2021). [find](https://scholar.google.com/scholar?q=E%2E+Chen%2C+Euclidean+geometry+in+mathematical+olympiads%2C+vol%2E+27+%28American+Mathematical+Soc%2E%29+%282021%29%2E)

*Updated 3 November 2026*