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

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

## Key facts

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

## Placed in

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

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

- [Open Source Prover in the Attic](https://mlsanity.com/paper/2401.13702/) (2024)

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

- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [A Comprehensive Survey of Scientific Large Language Models and Their Applications in Scientific Discovery](https://mlsanity.com/paper/2406.10833/) (2024)
- [OlympicArena: Benchmarking Multi-discipline Cognitive Reasoning for Superintelligent AI](https://mlsanity.com/paper/2406.12753/) (2024)
- [A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challenges](https://mlsanity.com/paper/2412.11936/) (2024)
- [Proposing and solving olympiad geometry with guided tree search](https://mlsanity.com/paper/2412.10673/) (2024)
- [OpenAI-o1 AB Testing: Does the o1 model really do good reasoning in math problem solving?](https://mlsanity.com/paper/2411.06198/) (2024)
- [Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions](https://mlsanity.com/paper/2512.00097/) (2025)
- [Quantum automated theorem proving](https://mlsanity.com/paper/2601.07953/) (2026)
- [Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discovery](https://mlsanity.com/paper/2606.08728/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4](https://mlsanity.com/paper/2608.02295/) (2026)

## Abstract (arXiv)

Proving geometric theorems constitutes a hallmark of visual reasoning combining both intuitive and logical skills. Therefore, automated theorem proving of Olympiad-level geometry problems is considered a notable milestone in human-level automated reasoning. The introduction of AlphaGeometry, a neuro-symbolic model trained with 100 million synthetic samples, marked a major breakthrough. It solved 25 of 30 International Mathematical Olympiad (IMO) problems whereas the reported baseline based on Wu's method solved only ten. In this note, we revisit the IMO-AG-30 Challenge introduced with AlphaGeometry, and find that Wu's method is surprisingly strong. Wu's method alone can solve 15 problems, and some of them are not solved by any of the other methods. This leads to two key findings: (i) Combining Wu's method with the classic synthetic methods of deductive databases and angle, ratio, and distance chasing solves 21 out of 30 methods by just using a CPU-only laptop with a time limit of 5 minutes per problem. Essentially, this classic method solves just 4 problems less than AlphaGeometry and establishes the first fully symbolic baseline strong enough to rival the performance of an IMO silver medalist. (ii) Wu's method even solves 2 of the 5 problems that AlphaGeometry failed to solve. Thus, by combining AlphaGeometry with Wu's method we set a new state-of-the-art for automated theorem proving on IMO-AG-30, solving 27 out of 30 problems, the first AI method which outperforms an IMO gold medalist.