The Gilbert-Pollak Conjecture \citep{gilbert1968steiner}, 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.

翻译：吉尔伯特-波拉克猜想 (Gilbert-Pollak Conjecture) \citep{gilbert1968steiner}，亦称斯坦纳比猜想 (Steiner Ratio Conjecture)，指出：对于欧几里得平面中的任意有限点集，其斯坦纳最小树长度至少为欧几里得最小生成树长度的 $\sqrt{3}/2 \approx 0.866$ 倍（即斯坦纳比）。经过20世纪80年代一系列改进，该猜想的下界被提升至 $0.824$，但此后三十年间未取得实质性进展。近年来，大型语言模型 (LLMs) 在竞赛级数学问题上展现出强大性能，但其解决开放式研究级问题的潜力仍鲜有探索。本研究提出一种新型人工智能系统，旨在获得斯坦纳比更紧的下界。该系统并非直接提示LLMs求解该猜想，而是要求其生成受规则约束的几何引理，并以可执行代码形式实现。这些引理随后被用于构建一组专用函数（称为验证函数），从而导出理论上可认证的斯坦纳比下界。通过基于反思的渐进式引理精化，该系统的斯坦纳比认证下界更新为 0.8559。整个研究过程仅涉及数千次LLM调用，充分展示了基于LLM的系统在高级数学研究领域的巨大潜力。