Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

The Gilbert-Pollak Conjecture, 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 $\sqrt{3}/2 \approx 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.

How can we connect locations with the shortest possible network, such as cables, roads, or communication links? A common baseline is the minimum spanning tree, which connects locations directly; adding extra junctions can make the network shorter. The Steiner ratio measures how short this improved network can be relative to the baseline. In 1968, Gilbert and Pollak conjectured that this ratio is always at least 0.866, but the best general lower bound had stayed at 0.824 since 1985. We study whether large language models can help make progress on this open problem. Rather than asking an AI system to prove the conjecture end to end, we let LLMs propose geometric lemmas within a structured, compositional space. These lemmas are converted into "verification functions" that certify a lower bound. When verification fails, the system identifies where the current lemmas are insufficient, guiding the next round of lemma proposals. This loop raises the certified lower bound for the Steiner ratio to 0.8559, close to the conjectured value 0.866. More broadly, the work suggests a practical pattern for AI-assisted mathematics: combine AI-generated modular proof ingredients with evaluators that provide rigorous assessment and targeted feedback, allowing the system to improve iteratively.