# Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

arXiv: https://arxiv.org/abs/2601.22365 · HTML: https://mlsanity.com/paper/2601.22365/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 38 references that are in the map.
- First posted on arXiv 29 Jan 2026.

## Builds on (most cited first, 12 of 12)

- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [OpenAI GPT-5 System Card](https://mlsanity.com/paper/2601.03267/) (2025)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search](https://mlsanity.com/paper/2504.08066/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Mini-o3: Scaling Up Reasoning Patterns and Interaction Turns for Visual Search](https://mlsanity.com/paper/2509.07969/) (2025)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience](https://mlsanity.com/paper/2512.17260/) (2025)

## Built on by (most cited first, 2 of 2)

- [Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics](https://mlsanity.com/paper/2606.17581/) (2026)
- [Semiotic Relations and Proof Methods: A Cross-Genre Study of Argument Structure with Large Language Models](https://mlsanity.com/paper/2609.15194/) (2026)

## 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.