{"ID":2835711,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2512.00097","arxiv_id":"2512.00097","title":"Gold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions","abstract":"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.","short_abstract":"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 wi...","url_abs":"https://arxiv.org/abs/2512.00097","url_pdf":"https://arxiv.org/pdf/2512.00097v1","authors":"[\"Boyan Duan\",\"Xiao Liang\",\"Shuai Lu\",\"Yaoxiang Wang\",\"Yelong Shen\",\"Kai-Wei Chang\",\"Ying Nian Wu\",\"Mao Yang\",\"Weizhu Chen\",\"Yeyun Gong\"]","published":"2025-11-27T01:05:00Z","proceeding":"cs.AI","tasks":"[\"cs.AI\",\"cs.CG\"]","methods":"[]","has_code":false}