Towards Solving the Gilbert-Pollak Conjecture via Large Language Models
Not on the map. Why?
Abstract (arXiv)
The Gilbert-Pollak Conjecture citepgilbert1968steiner, also known as the Steiner Ratio Conjecture, states that for any finite point set in the Euclidean plane, the Steiner minimum tree has length at least √3/2 ≈ 0.866 times that of the Euclidean minimum spanning tree (the Steiner ratio). A sequence of improvements through the 1980s culminated in a lower bound of 0.824, with no substantial progress reported over the past three decades. Recent advances in LLMs have demonstrated strong performance on contest-level mathematical problems, yet their potential for addressing open, research-level questions remains largely unexplored. In this work, we present a novel AI system for obtaining tighter lower bounds on the Steiner ratio. Rather than directly prompting LLMs to solve the conjecture, we task them with generating rule-constrained geometric lemmas implemented as executable code. These lemmas are then used to construct a collection of specialized functions, which we call verification functions, that yield theoretically certified lower bounds of the Steiner ratio. Through progressive lemma refinement driven by reflection, the system establishes a new certified lower bound of 0.8559 for the Steiner ratio. The entire research effort involves only thousands of LLM calls, demonstrating the strong potential of LLM-based systems for advanced mathematical research.
Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Builds on 12 of its 38 references that are in the map. First posted on arXiv 29 Jan 2026.
Builds on
12 of 38 references.
References · 12
- 2024The AI Scientist: Towards Fully Automated Open-Ended Scientific Discoverycited by 1,002
- 2025OpenAI GPT-5 System Cardcited by 910
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
- 2025The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Searchcited by 375
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
- 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
- 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
- 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
- 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
- 2025Mini-o3: Scaling Up Reasoning Patterns and Interaction Turns for Visual Searchcited by 116
- 2025Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2cited by 95
- 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
Built on by
Citing papers per year: 2026: 2.
2 papers.