# Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 36 references that are in the map.
- First posted on arXiv 27 Nov 2025.

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

- [GPT-4o System Card](https://mlsanity.com/paper/2410.21276/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [From System 1 to System 2: A Survey of Reasoning Large Language Models](https://mlsanity.com/paper/2502.17419/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [Beyond Pass@1: Self-Play with Variational Problem Synthesis Sustains RLVR](https://mlsanity.com/paper/2508.14029/) (2025)
- [SwS: Self-aware Weakness-driven Problem Synthesis in Reinforcement Learning for LLM Reasoning](https://mlsanity.com/paper/2506.08989/) (2025)
- [Proving Olympiad Algebraic Inequalities without Human Demonstrations](https://mlsanity.com/paper/2406.14219/) (2024)
- [Proposing and solving olympiad geometry with guided tree search](https://mlsanity.com/paper/2412.10673/) (2024)
- [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)

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

- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)

## Abstract (arXiv)

Automated theorem proving in Euclidean geometry, particularly for International Mathematical Olympiad (IMO) level problems, remains a major challenge and an important research focus in Artificial Intelligence. In this paper, we present a highly efficient method for geometry theorem proving that runs entirely on CPUs without relying on neural network-based inference. Our initial study shows that a simple random strategy for adding auxiliary points can achieve silver-medal level human performance on IMO. Building on this, we propose HAGeo, a Heuristic-based method for adding Auxiliary constructions in Geometric deduction that solves 28 of 30 problems on the IMO-30 benchmark, achieving gold-medal level performance and surpassing AlphaGeometry, a competitive neural network-based approach, by a notable margin. To evaluate our method and existing approaches more comprehensively, we further construct HAGeo-409, a benchmark consisting of 409 geometry problems with human-assessed difficulty levels. Compared with the widely used IMO-30, our benchmark poses greater challenges and provides a more precise evaluation, setting a higher bar for geometry theorem proving.