---
title: "Gold-medalist Performance in Solving Olympiad Geometry with"
description: "AlphaGeometry2 (AG2) is Google DeepMind's successor to AlphaGeometry (AG1), a neuro-symbolic… 40 references, cited by 28 papers here."
authors: ["Yuri Chervonyi", "Trieu H. Trinh", "Miroslav Olšák", "Xiaomeng Yang", "Hoang Nguyen", "Marcelo Menegali", "Junehyuk Jung", "Junsu Kim", "Vikas Verma", "Quoc V. Le", "Thang Luong"]
year: 2025
venue: "arXiv:2502.03544"
source: "https://arxiv.org/abs/2502.03544"
doi: "10.48550/arxiv.2502.03544"
arxiv: "2502.03544"
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/chervonyi-2025-gold-medalist-performance-solving-olympiad/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/chervonyi-2025-gold-medalist-performance-solving-olympiad/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/4/) / Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2

# Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2

**Authors:** [Yuri Chervonyi](https://md.research.elamur.ai/free/en/authors/yuri-chervonyi/), [Trieu H. Trinh](https://md.research.elamur.ai/free/en/authors/trieu-h-trinh/), [Miroslav Olšák](https://md.research.elamur.ai/free/en/authors/miroslav-olsak/), Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, [Junsu Kim](https://md.research.elamur.ai/free/en/authors/junsu-kim/), Vikas Verma, [Quoc V. Le](https://md.research.elamur.ai/free/en/authors/quoc-viet-le/) and [Thang Luong](https://md.research.elamur.ai/free/en/authors/thang-luong/) · **Year:** 2025 · **Venue:** arXiv:2502.03544 · **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/2502.03544) · [PDF](https://arxiv.org/pdf/2502.03544v3) · [DOI 10.48550/arxiv.2502.03544](https://doi.org/10.48550/arxiv.2502.03544) · [arXiv 2502.03544](https://arxiv.org/abs/2502.03544) · [OpenAlex](https://openalex.org/W4407244513)

**Citations:** 3 citations (OpenAlex, 2026-10-14) · [28](https://md.research.elamur.ai/free/en/papers/chervonyi-2025-gold-medalist-performance-solving-olympiad/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
AlphaGeometry2 (AG2) is Google DeepMind's successor to AlphaGeometry (AG1), a neuro-symbolic system for Euclidean geometry problems at International Mathematical Olympiad level. AG1 had three limitations: its formal language was narrow, its symbolic engine was slow, and its language model was modest. As a result, it solved only about half of recent IMO geometry tasks.

AG2 makes four main changes:
- **Language:** the formal language now covers "find the value" questions, linear relations between angles, distances and ratios, locus problems with moving objects, and non-constructive point definitions.
- **Symbolic engine:** the engine, DDAR, has a leaner rule set, better handling of coinciding points, and a much faster C++ implementation.
- **Language model:** a Gemini-based model is trained on a far larger and more varied synthetic corpus.
- **Search:** a new procedure, SKEST, runs several search trees that exchange discovered facts.

On IMO problems from 2000–2024, AG2 solves 84%, up from 54% for AG1. This exceeds the average gold medalist. AG2 also contributed to the system that reached silver-medal level at IMO 2024. The authors additionally show early steps towards a fully automatic pipeline: Gemini translates natural-language problems into the formal language, and a new algorithm generates the diagrams.

## Key points
- Coverage of the formal language on IMO 2000–2024 geometry rose from 66% to 88%. The remaining problems involve 3D geometry, inequalities, non-linear equations, or an arbitrary number of points.
- On the IMO-AG-50 benchmark, AG2 solves 42 of 50 problems. Its DDAR engine alone, without the language model, solves 16.
- The C++ DDAR implementation is roughly two orders of magnitude faster than the previous engine.
- SKEST (Shared Knowledge Ensemble of Search Trees) combines differently trained models, including math-pretrained ones fine-tuned on AlphaGeometry data, and this ensemble raises the solve rate.
- The public repository (google-deepmind/alphageometry2) contains the Python DDAR2 engine and 27 formalized IMO problems with diagrams and solutions in `test.py`. The Gemini training code and the full search code are not released.

*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

- [University of Cambridge](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) — University, Cambridge, United Kingdom · 287 works · 125,174 citations
- [Georgia Institute of Technology](https://md.research.elamur.ai/free/en/universities/georgia-institute-of-technology/) — University, Atlanta, United States · 159 works · 28,096 citations
- [Brown University](https://md.research.elamur.ai/free/en/universities/brown-university/) — University, Providence, United States · 85 works · 26,322 citations
- [Seoul National University](https://md.research.elamur.ai/free/en/universities/seoul-national-university/) — University, Seoul, South Korea · 47 works · 46,072 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: Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le and Thang Luong. 2025. Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2. arXiv:2502.03544.

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

```bibtex
@misc{chervonyi2025gold,
  title = {{Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2}},
  author = {Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Junsu Kim, Vikas Verma, Quoc V. Le and Thang Luong},
  year = {2025},
  doi = {10.48550/arxiv.2502.03544},
  eprint = {2502.03544},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2502.03544}
}
```

- [← previous FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://md.research.elamur.ai/free/en/papers/yu-2025-formalmath-benchmarking-formal-mathematical-reasoning/)
- [next → LiPO: Listwise Preference Optimization through Learning-to-Rank](https://md.research.elamur.ai/free/en/papers/liu-2025-lipo-listwise-preference-optimization-through/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/4/)

## References

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

1. H. Chae, S. Yoon, C. Y. Chun, G. Go, Y. Cho, G. Lee, and E. K. Ryu. Decomposing complex visual comprehension into atomic visual skills for vision language models. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS’24, 2024. URL [https://openreview.net/forum?id=nFU4xCyoe0](https://openreview.net/forum?id=nFU4xCyoe0) . [↗](https://openreview.net/forum?id=nFU4xCyoe0)
2. X. Chen, M. Lin, N. Schärli, and D. Zhou. Teaching large language models to self-debug. In The Twelfth International Conference on Learning Representations, 2024. URL [https://openreview.net/forum?id=KuPixIqPiq](https://openreview.net/forum?id=KuPixIqPiq) . [↗](https://openreview.net/forum?id=KuPixIqPiq)
3. S.-C. Chou. Proving and discovering geometry theorems using Wu’s method. The University of Texas at Austin, 1985. [find](https://scholar.google.com/scholar?q=S%2E%2DC%2E+Chou%2E+Proving+and+discovering+geometry+theorems+using+Wu%E2%80%99s+method%2E+The+University+of+Texas+at+Austin%2C+1985%2E)
4. S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. Automated production of traditional proofs for constructive geometry theorems. In [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pages 48–56. [find](https://scholar.google.com/scholar?q=S%2E%2DC%2E+Chou%2C+X%2E%2DS%2E+Gao%2C+and+J%2E%2DZ%2E+Zhang%2E+Automated+production+of+traditional+proofs+for+constructive+geometry+theorems%2E+In+%5B1993%5D+Proceedings+Eighth+Annual+IEEE+Symposium+on+Logic+in+Computer+Science%2C+)
5. S.-C. Chou, X. Gao, and J.-Z. Zhang. Machine proofs in geometry: Automated production of readable proofs for geometry theorems, volume 6. World Scientific, 1994. [find](https://scholar.google.com/scholar?q=S%2E%2DC%2E+Chou%2C+X%2E+Gao%2C+and+J%2E%2DZ%2E+Zhang%2E+Machine+proofs+in+geometry%3A+Automated+production+of+readable+proofs+for+geometry+theorems%2C+volume+6%2E+World+Scientific%2C+1994%2E)
6. S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. Automated generation of readable proofs with geometric invariants: I. multiple and shortest proof generation. Journal of Automated Reasoning, 17(3): 325–347, 1996. [find](https://scholar.google.com/scholar?q=S%2E%2DC%2E+Chou%2C+X%2E%2DS%2E+Gao%2C+and+J%2E%2DZ%2E+Zhang%2E+Automated+generation+of+readable+proofs+with+geometric+invariants%3A+I%2E+multiple+and+shortest+proof+generation%2E+Journal+of+Automated+Reasoning%2C+17%283%29%3A+325%E2%80%93347%2C+19)
7. S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 25(3):219–246, 2000. [find](https://scholar.google.com/scholar?q=S%2E%2DC%2E+Chou%2C+X%2E%2DS%2E+Gao%2C+and+J%2E%2DZ%2E+Zhang%2E+A+deductive+database+approach+to+automated+geometry+theorem+proving+and+discovering%2E+Journal+of+Automated+Reasoning%2C+25%283%29%3A219%E2%80%93246%2C+2000%2E)
8. B. Deiseroth, M. Brack, P. Schramowski, K. Kersting, and S. Weinbach. T-free: Tokenizer-free generative llms via sparse representations for memory-efficient embeddings, 2024. URL https://arxiv.org/abs/2406.19223 . — [arXiv:2406.19223](https://arxiv.org/abs/2406.19223) [↗](https://arxiv.org/abs/2406.19223)
9. Gemini Team. [Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context](https://md.research.elamur.ai/free/en/papers/gemini-team-2024-gemini-1-5-unlocking-multimodal/). arXiv preprint arXiv:2403.05530, 2024.
10. Y. Hu, W. Shi, X. Fu, D. Roth, M. Ostendorf, L. Zettlemoyer, N. A. Smith, and R. Krishna. Visual sketchpad: Sketching as a visual chain of thought for multimodal language models. In NeurIPS 2024 Workshop on Behavioral Machine Learning, 2024. URL [https://openreview.net/forum?id=prJ4b0GMSB](https://openreview.net/forum?id=prJ4b0GMSB) . [↗](https://openreview.net/forum?id=prJ4b0GMSB)
11. J. Huang, X. Chen, S. Mishra, H. S. Zheng, A. W. Yu, X. Song, and D. Zhou. [Large language models cannot self-correct reasoning yet](https://md.research.elamur.ai/free/en/papers/huang-2023-large-language-models-cannot-self/). In The Twelfth International Conference on Learning Representations, 2024. URL [https://openreview.net/forum?id=IkmD3fKBPQ](https://openreview.net/forum?id=IkmD3fKBPQ) . [↗](https://openreview.net/forum?id=IkmD3fKBPQ)
12. W. Jakob, J. Rhinelander, and D. Moldovan. pybind11 – seamless operability between c++11 and python, 2017. [https://github.com/pybind/pybind11](https://github.com/pybind/pybind11). [↗](https://github.com/pybind/pybind11)
13. P. Jha, P. Jana, P. Suresh, A. Arora, and V. Ganesh. Rlsf: Reinforcement learning via symbolic feedback, 2024. URL https://arxiv.org/abs/2405.16661 . [↗](https://arxiv.org/abs/2405.16661)
14. A. Q. Jiang, W. Li, and M. Jamnik. [Multilingual mathematical autoformalization](https://md.research.elamur.ai/free/en/papers/jiang-2023-multilingual-mathematical-autoformalization/). arXiv preprint arXiv:2311.03755, 2023.
15. D. Kapur. Geometry theorem proving using hilbert’s nullstellensatz. In Proceedings of the fifth ACM symposium on Symbolic and algebraic computation, pages 202–208, 1986a. [find](https://scholar.google.com/scholar?q=D%2E+Kapur%2E+Geometry+theorem+proving+using+hilbert%E2%80%99s+nullstellensatz%2E+In+Proceedings+of+the+fifth+ACM+symposium+on+Symbolic+and+algebraic+computation%2C+pages+202%E2%80%93208%2C+1986a%2E)
16. D. Kapur. Using gröbner bases to reason about geometry problems. Journal of Symbolic Computation, 2(4):399–408, 1986b. [find](https://scholar.google.com/scholar?q=D%2E+Kapur%2E+Using+gr%C3%B6bner+bases+to+reason+about+geometry+problems%2E+Journal+of+Symbolic+Computation%2C+2%284%29%3A399%E2%80%93408%2C+1986b%2E)
17. R. Krueger, J. M. Han, and D. Selsam. Automatically building diagrams for olympiad geometry problems. In CADE, pages 577–588, 2021. [find](https://scholar.google.com/scholar?q=R%2E+Krueger%2C+J%2E+M%2E+Han%2C+and+D%2E+Selsam%2E+Automatically+building+diagrams+for+olympiad+geometry+problems%2E+In+CADE%2C+pages+577%E2%80%93588%2C+2021%2E)
18. Z. Li, Z. Li, W. Tang, X. Zhang, Y. Yao, X. Si, F. Yang, K. Yang, and X. Ma. [Proving olympiad inequalities by synergizing LLMs and symbolic reasoning](https://md.research.elamur.ai/free/en/papers/li-2025-proving-olympiad-inequalities-synergizing-llms/). In The Thirteenth International Conference on Learning Representations, 2025. URL [https://openreview.net/forum?id=FiyS0ecSm0](https://openreview.net/forum?id=FiyS0ecSm0) . [↗](https://openreview.net/forum?id=FiyS0ecSm0)
19. H. Lightman, V. Kosaraju, Y. Burda, H. Edwards, B. Baker, T. Lee, J. Leike, J. Schulman, I. Sutskever, and K. Cobbe. Let’s verify step by step. In The Twelfth International Conference on Learning Representations, 2024. URL — [Let's Verify Step by Step](https://md.research.elamur.ai/free/en/papers/lightman-2023-let-s-verify-step-step/) [https://openreview.net/forum?id=v8L0pN6EOi](https://openreview.net/forum?id=v8L0pN6EOi) . [↗](https://openreview.net/forum?id=v8L0pN6EOi)
20. A. Madaan, N. Tandon, P. Gupta, S. Hallinan, L. Gao, S. Wiegreffe, U. Alon, N. Dziri, S. Prabhumoye, Y. Yang, S. Gupta, B. P. Majumder, K. Hermann, S. Welleck, A. Yazdanbakhsh, and P. Clark. Self-refine: Iterative refinement with self-feedback. In Thirty-seventh Conference on Neural Information Proc… [find](https://scholar.google.com/scholar?q=A%2E+Madaan%2C+N%2E+Tandon%2C+P%2E+Gupta%2C+S%2E+Hallinan%2C+L%2E+Gao%2C+S%2E+Wiegreffe%2C+U%2E+Alon%2C+N%2E+Dziri%2C+S%2E+Prabhumoye%2C+Y%2E+Yang%2C+S%2E+Gupta%2C+B%2E+P%2E+Majumder%2C+K%2E+Hermann%2C+S%2E+Welleck%2C+A%2E+Yazdanbakhsh%2C+and+P%2E+Clark%2E+Self%2Drefi)
21. S. Mouselinos, H. Michalewski, and M. Malinowski. Beyond lines and circles: Unveiling the geometric reasoning gap in large language models. In Y. Al-Onaizan, M. Bansal, and Y.-N. Chen, editors, Findings of the Association for Computational Linguistics: EMNLP 2024, pages 6192–6222, Miami, Florida, US… [find](https://scholar.google.com/scholar?q=S%2E+Mouselinos%2C+H%2E+Michalewski%2C+and+M%2E+Malinowski%2E+Beyond+lines+and+circles%3A+Unveiling+the+geometric+reasoning+gap+in+large+language+models%2E+In+Y%2E+Al%2DOnaizan%2C+M%2E+Bansal%2C+and+Y%2E%2DN%2E+Chen%2C+editors%2C+Findin)
22. L. Murphy, K. Yang, J. Sun, Z. Li, A. Anandkumar, and X. Si. [Autoformalizing euclidean geometry](https://md.research.elamur.ai/free/en/papers/murphy-2024-autoformalizing-euclidean-geometry/). In Forty-first International Conference on Machine Learning, 2024. URL [https://openreview.net/forum?id=bylZbZOsGA](https://openreview.net/forum?id=bylZbZOsGA) . [↗](https://openreview.net/forum?id=bylZbZOsGA)
23. S. Peng, D. Fu, Y. Liang, L. Gao, and Z. Tang. GeoDRL: A self-learning framework for geometry problem solving using reinforcement learning in deductive reasoning. In A. Rogers, J. Boyd-Graber, and N. Okazaki, editors, Findings of the Association for Computational Linguistics: ACL 2023, pages 13468–… [find](https://scholar.google.com/scholar?q=S%2E+Peng%2C+D%2E+Fu%2C+Y%2E+Liang%2C+L%2E+Gao%2C+and+Z%2E+Tang%2E+GeoDRL%3A+A+self%2Dlearning+framework+for+geometry+problem+solving+using+reinforcement+learning+in+deductive+reasoning%2E+In+A%2E+Rogers%2C+J%2E+Boyd%2DGraber%2C+and+N%2E+)
24. A. Poiroux, G. Weiss, V. Kunčak, and A. Bosselut. Improving autoformalization using type checking. arXiv preprint arXiv:2406.07222, 2024. [find](https://scholar.google.com/scholar?q=A%2E+Poiroux%2C+G%2E+Weiss%2C+V%2E+Kun%C4%8Dak%2C+and+A%2E+Bosselut%2E+Improving+autoformalization+using+type+checking%2E+arXiv+preprint+arXiv%3A2406%2E07222%2C+2024%2E)
25. S. Polu and I. Sutskever. [Generative language modeling for automated theorem proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/), 2020. URL https://arxiv.org/abs/2009.03393 . [↗](https://arxiv.org/abs/2009.03393)
26. N. Shinn, F. Cassano, A. Gopinath, K. R. Narasimhan, and S. Yao. [Reflexion: language agents with verbal reinforcement learning](https://md.research.elamur.ai/free/en/papers/shinn-2023-reflexion-language-agents-verbal-reinforcement/). In Thirty-seventh Conference on Neural Information Processing Systems, 2023. URL [https://openreview.net/forum?id=vAElhFcKW6](https://openreview.net/forum?id=vAElhFcKW6) . [↗](https://openreview.net/forum?id=vAElhFcKW6)
27. A. K. Singh and D. Strouse. [Tokenization counts: the impact of tokenization on arithmetic in frontier llms](https://md.research.elamur.ai/free/en/papers/singh-2024-tokenization-counts-impact-tokenization-arithmetic/), 2024. URL https://arxiv.org/abs/2402.14903 . [↗](https://arxiv.org/abs/2402.14903)
28. S. Sinha, A. Prabhu, P. Kumaraguru, S. Bhat, and M. Bethge. Wu’s method can boost symbolic ai to rival silver medalists and alphageometry to outperform gold medalists at imo geometry, 2024. [URL https://arxiv.org/abs/2404.06405](https://md.research.elamur.ai/free/en/papers/sinha-2024-wu-s-method-can-boost/). [↗](https://arxiv.org/abs/2404.06405)
29. K. Stechly, K. Valmeekam, and S. Kambhampati. [On the self-verification limitations of large language models on reasoning and planning tasks](https://md.research.elamur.ai/free/en/papers/stechly-2024-self-verification-limitations-large-language/). In The Thirteenth International Conference on Learning Representations, 2025. URL [https://openreview.net/forum?id=4O0v4s3IzY](https://openreview.net/forum?id=4O0v4s3IzY) . [↗](https://openreview.net/forum?id=4O0v4s3IzY)
30. C. Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings 13, pages 3–20. [find](https://scholar.google.com/scholar?q=C%2E+Szegedy%2E+A+promising+path+towards+autoformalization+and+general+artificial+intelligence%2E+In+Intelligent+Computer+Mathematics%3A+13th+International+Conference%2C+CICM+2020%2C+Bertinoro%2C+Italy%2C+July+26%E2%80%9331%2C)
31. T. H. Trinh, Y. Wu, Q. V. Le, H. He, and 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, 2024.
32. B. Tversky and M. Suwa. Thinking with sketches. In Tools for Innovation, pages 75–84. Oxford University Press, Nov. 2009. [find](https://scholar.google.com/scholar?q=B%2E+Tversky+and+M%2E+Suwa%2E+Thinking+with+sketches%2E+In+Tools+for+Innovation%2C+pages+75%E2%80%9384%2E+Oxford+University+Press%2C+Nov%2E+2009%2E)
33. X. Wang, Y. Wang, W. Zhu, and R. Wang. Do large language models truly understand geometric structures? In The Thirteenth International Conference on Learning Representations, 2025. URL [https://openreview.net/forum?id=FjQOXenaXK](https://openreview.net/forum?id=FjQOXenaXK) . [↗](https://openreview.net/forum?id=FjQOXenaXK)
34. C. Wei, M. Sun, and W. Wang. [Proving olympiad algebraic inequalities without human demonstrations](https://md.research.elamur.ai/free/en/papers/wei-2024-proving-olympiad-algebraic-inequalities-without/). In The Thirty-eight Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2024. URL [https://openreview.net/forum?id=8kFctyli9H](https://openreview.net/forum?id=8kFctyli9H) . [↗](https://openreview.net/forum?id=8kFctyli9H)
35. W.-t. Wu. On the decision problem and the mechanization of theorem-proving in elementary geometry. In Selected Works Of Wen-Tsun Wu, pages 117–138. World Scientific, 2008. [find](https://scholar.google.com/scholar?q=W%2E%2Dt%2E+Wu%2E+On+the+decision+problem+and+the+mechanization+of+theorem%2Dproving+in+elementary+geometry%2E+In+Selected+Works+Of+Wen%2DTsun+Wu%2C+pages+117%E2%80%93138%2E+World+Scientific%2C+2008%2E)
36. Y. Wu, A. Q. Jiang, W. Li, M. N. Rabe, C. Staats, M. Jamnik, and C. Szegedy. [Autoformalization with large language models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/), 2022. URL https://arxiv.org/abs/2205.12615 . [↗](https://arxiv.org/abs/2205.12615)
37. Y. Yan, Y. Lu, R. Xu, and Z. Lan. Do phd-level llms truly grasp elementary addition? probing rule learning vs. memorization in large language models, 2025. URL https://arxiv.org/abs/2504.05262 . — [arXiv:2504.05262](https://arxiv.org/abs/2504.05262) [↗](https://arxiv.org/abs/2504.05262)
38. C. Zhang, J. Song, S. Li, Y. Liang, Y. Ma, W. Wang, Y. Zhu, and S.-C. Zhu. [Proposing and solving olympiad geometry with guided tree search](https://md.research.elamur.ai/free/en/papers/zhang-2024-proposing-solving-olympiad-geometry-guided/). arXiv preprint arXiv:2412.10673, 2024.
39. L. Zhang, A. Hosseini, H. Bansal, M. Kazemi, A. Kumar, and R. Agarwal. [Generative verifiers: Reward modeling as next-token prediction](https://md.research.elamur.ai/free/en/papers/zhang-2024-generative-verifiers-reward-modeling-as/). In The Thirteenth International Conference on Learning Representations, 2025. URL [https://openreview.net/forum?id=Ccwp4tFEtE](https://openreview.net/forum?id=Ccwp4tFEtE) . [↗](https://openreview.net/forum?id=Ccwp4tFEtE)
40. Case 8 9 7 4 Auxiliary constructions will be the following points and everything else they depend on 𝑏, 𝑐, 𝑑 𝑐, 𝑑 𝑏, 𝑐 𝑎 𝑎 Then if X is nonempty, we create a synthetic proof that says: "when X moves, ... 𝑎 moves on a fixed line 𝑏 & 𝑐 are equidistant to a fixed point, circle center 𝑏 , radius 𝑐𝑑 goes… [find](https://scholar.google.com/scholar?q=Case+8+9+7+4+Auxiliary+constructions+will+be+the+following+points+and+everything+else+they+depend+on+%F0%9D%91%8F%2C+%F0%9D%91%90%2C+%F0%9D%91%91+%F0%9D%91%90%2C+%F0%9D%91%91+%F0%9D%91%8F%2C+%F0%9D%91%90+%F0%9D%91%8E+%F0%9D%91%8E+Then+if+X+is+nonempty%2C+we+create+a+synthetic+proof+that+says%3A+%22when+X+moves%2C+)

*Updated 3 November 2026*