mlsanityData to 7 Oct 2026

Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

arXiv 2601.22365 ↗First posted 29 Jan 2026cs.DM cs.LGcited by 2

Not on the map. Why?

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.

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

Builds on

12 of 38 references.

References · 12

  1. 2024The AI Scientist: Towards Fully Automated Open-Ended Scientific Discoverycited by 1,002
  2. 2025OpenAI GPT-5 System Cardcited by 910
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2025The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Searchcited by 375
  5. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  6. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  7. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  8. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  9. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  10. 2025Mini-o3: Scaling Up Reasoning Patterns and Interaction Turns for Visual Searchcited by 116
  11. 2025Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2cited by 95
  12. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 2.

2 papers.