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.

翻译：吉尔伯特-波拉克猜想（又称斯坦纳比猜想）指出：对于欧氏平面上的任意有限点集，斯坦纳最小树的长度至少是欧几里得最小生成树长度的$\sqrt{3}/2 \approx 0.866$倍（该比值称为斯坦纳比）。上世纪八十年代通过一系列改进将下界提升至0.824后，过去三十年间未取得实质性进展。近期大型语言模型在竞赛级数学问题上展现出卓越性能，但其解决开放性研究级问题的潜力尚未得到充分探索。本研究提出一种新型人工智能系统，用于获得更紧致的斯坦纳比下界。我们并非直接要求大型语言模型求解猜想，而是让其生成可转化为可执行代码的规则约束几何引理。这些引理被用于构建一组专用函数（称为验证函数），可产出理论验证的斯坦纳比下界。通过反思驱动的渐进式引理优化，该系统为斯坦纳比建立了0.8559的新验证下界。整个研究过程仅需数千次大型语言模型调用，彰显了基于大型语言模型的系统在高等数学研究中的强大潜力。