Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

2026/01/29 by Yisi Ke, Tianyu Huang, Yankai Shu +3 · 1 voice · 1 citation
Computer Science · #cs.DM #cs.LG

paper · pdf · doi:10.48550/arxiv.2601.22365

arxiv published 2026/01/29 · arxiv updated 2026/05/21

Abstract

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.

Citations

• Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
• OpenAI GPT-5 System Card
• Mini-o3: Scaling Up Reasoning Patterns and Interaction Turns for Visual Search
• Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
• The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
• Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2
• DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
• The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
• Scaling deep learning for materials discovery
• Learning skillful medium-range global weather forecasting
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
• HyperTree Proof Search for Neural Theorem Proving
• Highly accurate protein structure prediction with AlphaFold
• A NEW BOUND FOR EUCLIDEAN STEINER MINIMAL TREES
• OpenAI o1 System Card

Cited by

• Autonomous Discovery of Particle Physics Theories from Experimental Data

Discussions

• Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang: Towards Solving the Gilbert-Pollak Conjecture via Large Language Models https://arxiv.org/abs/2601.22365 https://arxiv.org/pdf/2601.2 [bsky, 0 points, 0 comments]

Related

• Improved Inapproximability Results for Steiner Tree via Long Code Based Reductions
• Strong Steiner Tree Approximations in Practice
• Prize-Collecting Steiner Tree: A 1.79 Approximation
• Mining Math Conjectures from LLMs: A Pruning Approach
• A note on Johnson, Minkoff and Phillips' algorithm for the Prize-Collecting Steiner Tree Problem