---
title: "Wu's Method can Boost Symbolic AI to Rival Silver Medalists and"
description: "Automated proving of olympiad geometry is often treated as a milestone for machine reasoning. 28 references, cited by 6 papers here."
authors: ["Shiven Sinha", "Ameya Prabhu", "Ponnurangam Kumaraguru", "Siddharth Bhat", "Matthias Bethge"]
year: 2024
venue: "arXiv:2404.06405"
source: "https://arxiv.org/abs/2404.06405"
doi: "10.48550/arxiv.2404.06405"
arxiv: "2404.06405"
licence: "CC BY 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/sinha-2024-wu-s-method-can-boost/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/sinha-2024-wu-s-method-can-boost/)

[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/10/) / Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry

# Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry

**Authors:** Shiven Sinha, [Ameya Prabhu](https://md.research.elamur.ai/free/en/authors/ameya-prabhu/), [Ponnurangam Kumaraguru](https://md.research.elamur.ai/free/en/authors/ponnurangam-kumaraguru/), Siddharth Bhat and Matthias Bethge · **Year:** 2024 · **Venue:** arXiv:2404.06405 · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/)

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

**Citations:** 1 citations (OpenAlex, 2026-10-14) · 6 in our library, of the 149,439 papers whose bibliographies we read

## Summary
Automated proving of olympiad geometry is often treated as a milestone for machine reasoning. AlphaGeometry is a neuro-symbolic system trained on 100 million synthetic proofs. It solved 25 of the 30 problems in the IMO-AG-30 benchmark, while the Wu's method baseline reported alongside it managed only ten. The authors revisit this algebraic technique, which turns geometric premises and goals into polynomial equations. They manually rewrote the benchmark problems for the JGEX software, and 26 of the 30 could be expressed there. They also reproduced the DD+AR symbolic engine from the AlphaGeometry codebase. Wu's method alone proved 15 problems, mostly within seconds on an ordinary laptop. Combining it with DD+AR yields Wu&DD+AR, a system with no neural component that solves 21 problems, close to silver-medalist level. Wu's method also handles two problems AlphaGeometry missed, so a simple ensemble, Wu&AG, reaches 27 of 30 and exceeds the average gold medalist. The authors argue that algebraic provers complement synthetic and LLM-based approaches. In their view, these provers have been undervalued even though they do not yield human-readable proofs.

## Key points
- Wu's method solved 15 problems on IMO-AG-30, up from the 10 previously reported. Evaluation covered the 26 problems translatable into JGEX. Fourteen were solved in under 5 seconds, and 2015 P4 took about 3 minutes. Unsolved cases usually exhausted memory within 5 minutes.
- Hardware was a CPU-only laptop with an AMD Ryzen 7 5800H and 16 GB RAM, using a 5-minute limit per problem.
- Wu&DD+AR solves 21/30. That is 6 more than the best earlier traditional method and equal to AlphaGeometry without fine-tuning (FT-9M only).
- Wu&AG solves 27/30. Problems 2008 P1B and 2021 P3 are solved by no prover other than Wu's method. Human reference averages are 15.2 for all contestants, 19.3 for bronze, 22.9 for silver and 25.9 for gold.
- The problem translations are released at huggingface.co/datasets/bethgelab/simplegeometry. The authors note that existing algebraic tools are limited, mainly through missing constructions and weak performance.

*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 · 243 works · 121,396 citations
- [University of Tübingen](https://md.research.elamur.ai/free/en/universities/university-of-tubingen/) — University, Tübingen, Germany · 75 works · 41,081 citations
- [International Institute of Information Technology, Hyderabad](https://md.research.elamur.ai/free/en/universities/international-institute-of-information-technology-hyderabad/) — University, Hyderabad, India · 38 works · 1,821 citations
- [Tübingen AI Center](https://md.research.elamur.ai/free/en/universities/tubingen-ai-center/) — University, Tübingen, Germany · 3 works · 30 citations

📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 16,667 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 16,194 works · [➗ Mathematics](https://md.research.elamur.ai/free/en/shelves/mathematics/) · 177 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 252 works · [➗ Geometry and Topology](https://md.research.elamur.ai/free/en/shelves/mathematics/geometry-and-topology/) · 3 works

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

💡 Concepts (1): [💡 Artificial intelligence](https://md.research.elamur.ai/free/en/concepts/artificial-intelligence/) · 49 works

## Cite

Cite as: Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat and Matthias Bethge. 2024. Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry. arXiv:2404.06405.

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

```bibtex
@misc{sinha2024wu,
  title = {{Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry}},
  author = {Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat and Matthias Bethge},
  year = {2024},
  doi = {10.48550/arxiv.2404.06405},
  eprint = {2404.06405},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2404.06405}
}
```

- [← previous Towards Fine-Grained Pedagogical Control over English Grammar Complexity in Educational Text Generation](https://md.research.elamur.ai/free/en/papers/glandorf-2024-fine-grained-pedagogical-control-over/)
- [next → Annotating FrameNet via Structure-Conditioned Language Generation](https://md.research.elamur.ai/free/en/papers/cui-2024-annotating-framenet-structure-conditioned-language/)
- [↑ back to papers of 2024](https://md.research.elamur.ai/free/en/papers/2024/page/10/)

## References

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

1. Aimo prize. [https://aimoprize.com/](https://aimoprize.com/). 1 [↗](https://aimoprize.com/)
2. Imo grand challenge. [https://imo-grand-challenge.github.io/](https://imo-grand-challenge.github.io/). 1 [↗](https://imo-grand-challenge.github.io/)
3. Peter novotný’s masters thesis. [https://skmo.sk/cvika/ukazpdf.php?pdf=diplomka.pdf](https://skmo.sk/cvika/ukazpdf.php?pdf=diplomka.pdf). 4 [↗](https://skmo.sk/cvika/ukazpdf.php?pdf=diplomka.pdf)
4. Jeremy Avigad, Edward Dean, and John Mumma. A formal system for euclid’s elements. The Review of Symbolic Logic, 2009. 1 [find](https://scholar.google.com/scholar?q=Jeremy+Avigad%2C+Edward+Dean%2C+and+John+Mumma%2E+A+formal+system+for+euclid%E2%80%99s+elements%2E+The+Review+of+Symbolic+Logic%2C+2009%2E+1)
5. Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, and Julien Narboux. Geocoq. 2018. 1 [find](https://scholar.google.com/scholar?q=Michael+Beeson%2C+Pierre+Boutry%2C+Gabriel+Braun%2C+Charly+Gries%2C+and+Julien+Narboux%2E+Geocoq%2E+2018%2E+1)
6. 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, 2000. doi: 10.1023/A:1006171315513. 2 [find](https://scholar.google.com/scholar?q=S%2EC%2E+Chou%2C+X%2ES%2E+Gao%2C+and+J%2EZ%2E+Zhang%2E+A+deductive+database+approach+to+automated+geometry+theorem+proving+and+discovering%2E+Journal+of+Automated+Reasoning%2C+2000%2E+doi%3A+10%2E1023%2FA%3A1006171315513%2E+2)
7. Shang-Ching Chou. Proving elementary geometry theorems using wu’s algorithm. In Woodrow Wilson Bledsoe and Donald W Loveland, editors, Automated Theorem Proving: After 25 Years, volume 89. American Mathematical Soc., 1984. 2 [find](https://scholar.google.com/scholar?q=Shang%2DChing+Chou%2E+Proving+elementary+geometry+theorems+using+wu%E2%80%99s+algorithm%2E+In+Woodrow+Wilson+Bledsoe+and+Donald+W+Loveland%2C+editors%2C+Automated+Theorem+Proving%3A+After+25+Years%2C+volume+89%2E+American+Ma)
8. Shang-Ching Chou. An introduction to wu’s method for mechanical theorem proving in geometry. Journal of Automated Reasoning, 1988. 2 [find](https://scholar.google.com/scholar?q=Shang%2DChing+Chou%2E+An+introduction+to+wu%E2%80%99s+method+for+mechanical+theorem+proving+in+geometry%2E+Journal+of+Automated+Reasoning%2C+1988%2E+2)
9. Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. Automated production of traditional proofs in solid geometry. Journal of Automated Reasoning, 14(2):257–291, 1995. 2 [find](https://scholar.google.com/scholar?q=Shang%2DChing+Chou%2C+Xiao%2DShan+Gao%2C+and+Jing%2DZhong+Zhang%2E+Automated+production+of+traditional+proofs+in+solid+geometry%2E+Journal+of+Automated+Reasoning%2C+14%282%29%3A257%E2%80%93291%2C+1995%2E+2)
10. Nicolaas Govert de Bruijn. AUTOMATH, a language for mathematics. 1983. 1 [find](https://scholar.google.com/scholar?q=Nicolaas+Govert+de+Bruijn%2E+AUTOMATH%2C+a+language+for+mathematics%2E+1983%2E+1)
11. Giuseppa Carr‘a Ferro, Giovanni Gallo, and Rosario Gennaro. Probabilistic verification of elementary geometry statements. In Automated Deduction in Geometry, 1997. doi: 10.1007/BFb0022721. 1 — [doi:10.1007/bfb0022721](https://doi.org/10.1007/bfb0022721) [find](https://scholar.google.com/scholar?q=Giuseppa+Carr%E2%80%98a+Ferro%2C+Giovanni+Gallo%2C+and+Rosario+Gennaro%2E+Probabilistic+verification+of+elementary+geometry+statements%2E+In+Automated+Deduction+in+Geometry%2C+1997%2E+doi%3A+10%2E1007%2FBFb0022721%2E+1+%E2%80%94+%5Bdoi%3A10)
12. H. Gelernter. Realization of a geometry-theorem proving machine. Computers & Thought, 1995. doi: 10.5555/ 207644.207647. 1, 2 [find](https://scholar.google.com/scholar?q=H%2E+Gelernter%2E+Realization+of+a+geometry%2Dtheorem+proving+machine%2E+Computers+%26+Thought%2C+1995%2E+doi%3A+10%2E5555%2F+207644%2E207647%2E+1%2C+2)
13. W. T. Gowers. How can it be feasible to find proofs? [https://drive.google.com/file/d/](https://drive.google.com/file/d/) 1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view. Accessed: 7 April 2024. 2 [↗](https://drive.google.com/file/d/)
14. Thomas Little Heath et al. The thirteen books of Euclid’s Elements. 1956. 1 [find](https://scholar.google.com/scholar?q=Thomas+Little+Heath+et+al%2E+The+thirteen+books+of+Euclid%E2%80%99s+Elements%2E+1956%2E+1)
15. Deepak Kapur. Using gröbner bases to reason about geometry problems. Journal of Symbolic Computation, 1986. 2 [find](https://scholar.google.com/scholar?q=Deepak+Kapur%2E+Using+gro%CC%88bner+bases+to+reason+about+geometry+problems%2E+Journal+of+Symbolic+Computation%2C+1986%2E+2)
16. Deepak Kapur. A refutational approach to geometry theorem proving. Artificial Intelligence, 1988. 2 [find](https://scholar.google.com/scholar?q=Deepak+Kapur%2E+A+refutational+approach+to+geometry+theorem+proving%2E+Artificial+Intelligence%2C+1988%2E+2)
17. Michelle Y. Kim. Visual reasoning in geometry theorem proving. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, 1989. 1 [find](https://scholar.google.com/scholar?q=Michelle+Y%2E+Kim%2E+Visual+reasoning+in+geometry+theorem+proving%2E+In+Proceedings+of+the+Eleventh+International+Joint+Conference+on+Artificial+Intelligence%2C+1989%2E+1)
18. Zoltán Kovács and Alexander Vujic. Open source prover in the attic. arXiv preprint arXiv:2401.13702, 2024. 3 — [arXiv:2401.13702](https://arxiv.org/abs/2401.13702) [find](https://scholar.google.com/scholar?q=Zolta%CC%81n+Kova%CC%81cs+and+Alexander+Vujic%2E+Open+source+prover+in+the+attic%2E+arXiv+preprint+arXiv%3A2401%2E13702%2C+2024%2E+3+%E2%80%94+%5BarXiv%3A2401%2E13702%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F2401%2E13702%29)
19. Zoltán Kovács, Tomas Recio, Luis F Tabera, and M Pilar Vélez. Dealing with degeneracies in automated theorem proving in geometry. Mathematics, 2021. 2 [find](https://scholar.google.com/scholar?q=Zolta%CC%81n+Kova%CC%81cs%2C+Tomas+Recio%2C+Luis+F+Tabera%2C+and+M+Pilar+Ve%CC%81lez%2E+Dealing+with+degeneracies+in+automated+theorem+proving+in+geometry%2E+Mathematics%2C+2021%2E+2)
20. Arthur J Nevins. Plane geometry theorem proving using forward chaining. Artificial Intelligence, 6(1):1–23, 1975. 2 [find](https://scholar.google.com/scholar?q=Arthur+J+Nevins%2E+Plane+geometry+theorem+proving+using+forward+chaining%2E+Artificial+Intelligence%2C+6%281%29%3A1%E2%80%9323%2C+1975%2E+2)
21. Jürgen Richter-Gebert and Ulrich Kortenkamp. The Interactive Geometry Software Cinderella. 1999. 1 [find](https://scholar.google.com/scholar?q=Ju%CC%88rgen+Richter%2DGebert+and+Ulrich+Kortenkamp%2E+The+Interactive+Geometry+Software+Cinderella%2E+1999%2E+1)
22. Max Schindler and Evan Chen. Barycentric coordinates in olympiad geometry. Olympiad Articles, 2012. 1 [find](https://scholar.google.com/scholar?q=Max+Schindler+and+Evan+Chen%2E+Barycentric+coordinates+in+olympiad+geometry%2E+Olympiad+Articles%2C+2012%2E+1)
23. Justin Stevens. Coordinate and trigonometry bashing. [http://services.artofproblemsolving.com/](http://services.artofproblemsolving.com/) download.php?id=YXR0YWNobWVudHMvYi9kLzRmMTA5OWJhNmI1MTg2YzM2ODdkZTVhYTJjMGU0NjdmYmViNGRk&rn= Q29vcmRpbmF0ZSBhbmQgVHJpZ29ub21ldHJ5IEJhc2hpbmcucGRm. Accessed: 4 April 2024. 1 [↗](http://services.artofproblemsolving.com/)
24. Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. [Solving olympiad geometry without human demonstrations](https://md.research.elamur.ai/free/en/papers/trinh-2024-solving-olympiad-geometry-without-human/). Nature, 2024. 2, 3, 7
25. Dongming Wang. Reasoning about geometric problems using an elimination method. Automated practical reasoning: Algebraic approaches, pages 147–185, 1995. 2 [find](https://scholar.google.com/scholar?q=Dongming+Wang%2E+Reasoning+about+geometric+problems+using+an+elimination+method%2E+Automated+practical+reasoning%3A+Algebraic+approaches%2C+pages+147%E2%80%93185%2C+1995%2E+2)
26. Wu Wen-Tsün. On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica, 1978. 2 [find](https://scholar.google.com/scholar?q=Wu+Wen%2DTsu%CC%88n%2E+On+the+decision+problem+and+the+mechanization+of+theorem+proving+in+elementary+geometry%2E+Scientia+Sinica%2C+1978%2E+2)
27. Wenjun Wu. On zeros of algebraic equations–an application of ritt principle. Kexue Tongbao, 1986. 2 [find](https://scholar.google.com/scholar?q=Wenjun+Wu%2E+On+zeros+of+algebraic+equations%E2%80%93an+application+of+ritt+principle%2E+Kexue+Tongbao%2C+1986%2E+2)
28. Z. Ye, S.C. Chou, and X.S. Gao. An introduction to java geometry expert – (extended abstract). 2011. doi: 10.1007/978-3-642-21046-4 10. 3 — [doi:10.1007/978-3-642-21046-4](https://doi.org/10.1007/978-3-642-21046-4) [find](https://scholar.google.com/scholar?q=Z%2E+Ye%2C+S%2EC%2E+Chou%2C+and+X%2ES%2E+Gao%2E+An+introduction+to+java+geometry+expert+%E2%80%93+%28extended+abstract%29%2E+2011%2E+doi%3A+10%2E1007%2F978%2D3%2D642%2D21046%2D4+10%2E+3+%E2%80%94+%5Bdoi%3A10%2E1007%2F978%2D3%2D642%2D21046%2D4%5D%28https%3A%2F%2Fdoi%2Eorg%2F10%2E1007%2F978%2D)

*Updated 30 October 2026*