💻 computer science

Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

This paper presents an AI system that leverages large language models to generate and refine executable geometric lemmas, achieving a new certified lower bound of 0.8559 for the Steiner ratio and making significant progress toward the long-standing Gilbert-Pollak Conjecture.

Original authors: Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

Published 2026-05-22

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a city planner trying to connect a group of houses with roads. You have two ways to do this:

The "Direct" Way (Minimum Spanning Tree): You connect the houses directly to each other. You can't build any new intersections; you just draw lines between the existing houses.
The "Smart" Way (Steiner Minimal Tree): You are allowed to build new, invisible intersections (called Steiner points) anywhere in the city. By adding these extra hubs, you can often create a network that is shorter and uses less asphalt than the direct way.

The Big Question:
How much shorter can the "Smart" way be compared to the "Direct" way?

In 1968, mathematicians Gilbert and Pollak made a famous guess (a conjecture). They said: "No matter how you arrange the houses, the Smart Way will never be less than 86.6% (specifically $\sqrt{3}/2$ ) of the length of the Direct Way."

For decades, mathematicians tried to prove this. They managed to prove it was at least 82.4% of the length, but they got stuck there. The math problem was like a giant, tangled knot that human brains couldn't untangle because there were too many possible shapes and angles to check.

The New Approach: The AI "Lemma Factory"
This paper describes a new system where an AI (a Large Language Model) helps solve this knot. But the AI doesn't try to solve the whole problem at once—that would be like asking a robot to write a whole novel in one second. Instead, the researchers built a specialized factory for the AI.

Here is how the system works, using a simple analogy:

1. The "Proof" is a Giant Jigsaw Puzzle

To prove the 86.6% rule, you have to check every possible shape the road network could take. This is impossible to do one by one.
Instead, mathematicians use a strategy called induction. They say: "If we can prove that any time we cut a piece off the network, the remaining piece still follows the rules, then the whole thing follows the rules."

To do this, they need tiny, specific rules called lemmas. Think of a lemma as a single, perfect puzzle piece that says, "If the roads look like this, then we know for sure the length is at least that."

2. The AI's Job: Making the Puzzle Pieces

The researchers didn't ask the AI to solve the whole puzzle. They asked it to do something much smaller: Write code that generates these puzzle pieces.

The Constraint: The AI is told, "You can only write code that describes a specific geometric shape (like a 'Trapped Regular Point' or a '4-Point Tree')."
The Output: The AI writes a small program (a "lemma") that says, "If the road lengths are $X, Y, Z$ , then the total length is bounded by $W$ ."
The Safety Net: The AI's code isn't trusted blindly. It is fed into a strict mathematical calculator (like a super-precise calculator called Mathematica). If the calculator says the code is wrong, the AI tries again. If it says "Correct," the piece is added to the collection.

3. The "Reflection" Loop: Finding the Weak Spots

This is the clever part. The system doesn't just guess randomly.

The system tries to prove the 86.6% rule using the current collection of puzzle pieces.
It fails. It finds a specific "bottleneck"—a weird shape of roads where the current pieces don't fit.
The system tells the AI: "Hey, you failed here. Look at this specific shape. Go write a new puzzle piece that fits this exact spot."
The AI generates a new lemma, the calculator checks it, and if it works, the system tries again.

It's like a video game where you keep hitting a wall, and the game tells you exactly where to build a bridge to get past it.

The Result

After about 10 rounds of this "try, fail, reflect, improve" loop, the system built a collection of puzzle pieces so strong that it could finally prove a new, tighter rule:

The Smart Way is at least 85.59% of the length of the Direct Way.

This is a massive improvement over the previous record of 82.4%, which had stood for nearly 40 years.

Why This Matters (According to the Paper)

It's Cheap: The whole research project only cost a few hundred dollars in computer time.
It's Fast: It took the AI only a few days of "thinking" (and a few thousand calls to the model) to do what humans couldn't do in decades.
It's Rigorous: The AI didn't just "guess." It generated code that was mathematically verified to be 100% correct. The final proof is a standard mathematical proof that stands on its own, independent of the AI.

In short: The researchers didn't ask an AI to be a genius mathematician. They asked it to be a brilliant, tireless assistant that builds tiny, verified tools (lemmas) to help humans solve a problem that was previously too big to crack. They turned a "black box" AI into a transparent, step-by-step discovery engine.

Technical Summary: Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

1. Problem Statement

The paper addresses the Gilbert-Pollak Conjecture (1968), a seminal open problem in combinatorial optimization and computational geometry. The conjecture posits that for any finite set of points in the Euclidean plane, the ratio between the length of the Steiner Minimal Tree (SMT) and the Euclidean Minimum Spanning Tree (MST) is lower-bounded by $\sqrt{3}/2 \approx 0.866$ . This ratio is known as the Steiner ratio.

While the conjecture has been verified for small numbers of points ( $n \le 6$ ), the general lower bound for arbitrary $n$ has remained stagnant since 1985. The previous state-of-the-art lower bound, established by Chung & Graham (1985), is 0.824. Progress has stalled due to the combinatorial explosion of topological structures required for analysis and the intractability of the geometric verification involved in manual derivation.

The authors investigate whether Large Language Models (LLMs), which have shown proficiency in contest-level mathematics, can be extended to tackle such open, research-level conjectures. They note that naively prompting LLMs to solve the conjecture directly often results in hallucinations and logical gaps due to the vast, unconstrained search space and the scarcity of research-level concepts in training data.

2. Methodology

The authors propose a novel AI system that avoids direct end-to-end proof generation. Instead, the system decomposes the problem into a structured, iterative discovery process driven by verification functions and reflection.

2.1. The Verification Framework

The core mathematical strategy relies on an induction-based reduction argument (Du & Hwang, 1983). To prove a lower bound $\rho$ , one must show that for any geometric configuration $w$ , there exists a "splitting" of the tree such that a specific splitting function $F_\tau(w, \rho) \le 0$ .

Verification Functions: To make the continuous minimax problem tractable, the system introduces verification functions. These are upper bounds of splitting functions that satisfy specific structural constraints (unimodality along coordinate axes).
Vertex Maximum Property: A key theoretical contribution is proving that for these verification functions, the global maximum over a bounded hyperrectangle is attained at one of its vertices. This reduces the verification of an infinite continuous domain to a finite set of vertex checks.
Branch-and-Bound: The system employs a Branch-and-Bound algorithm to recursively partition the parameter space, verifying the condition at vertices and checking monotonicity for unbounded regions.

2.2. LLM Agent and Lemma Generation

Rather than asking the LLM to prove the conjecture, the system tasks it with generating rule-constrained geometric lemmas implemented as executable code. The search space is narrowed to two specific types of lemmas:

Trapped Regular Point Lemmas: Proving that under certain linear constraints, an implicit regular point is confined within a bounded polygonal region, allowing for distance bounds.
Valid 4-Point Steiner Tree Lemmas: Proving that under specific orthogonally convex conditions, a specific 4-point Steiner tree topology is valid, allowing for exact length calculations.

The LLM agent operates in a loop:

Selection: It selects relevant geometric predicates (Type A: intrinsic properties; Type B: sufficient trapping conditions) from a predefined set.
Derivation: It uses symbolic tools (Mathematica) to derive the implications of these predicates.
Simplification: It simplifies complex algebraic regions into linear or orthogonally convex constraints suitable for the reward model.
Coding: It outputs the derived conditions as C++ functions (X_cond, AX_upper_bound, etc.) that serve as the verification functions.

2.3. Iterative Reflection Mechanism

The system utilizes a targeted reflection mechanism to overcome bottlenecks:

Evaluation: The reward model attempts to certify a candidate lower bound $\rho$ .
Bottleneck Identification: If verification fails, the system identifies the specific "bottleneck region" (a set of uncertified hyperrectangles) where the current lemmas are insufficient.
Feedback: This region is converted into a structured prompt, instructing the LLM to generate new lemmas specifically targeting the geometric constraints of this bottleneck.
Refinement: The new lemmas are validated and added to the set of verification functions, and the process repeats.

3. Key Contributions

Novel AI System for Theoretical Discovery: The paper presents a system that successfully automates the discovery of intermediate geometric lemmas for a decades-old open problem, moving beyond standard contest-level problem solving.
Verification Functions and Vertex Property: The authors formally define verification functions and prove the "Vertex Maximum Property," which enables rigorous, computationally tractable verification of lower bounds over continuous domains.
Decomposition Strategy: By decomposing the conjecture into the generation of specific, rule-constrained lemmas (Trapped Points and Valid 4-Point Trees) rather than full proofs, the system effectively manages the search space and minimizes hallucinations.
Bottleneck-Driven Reflection: The introduction of a reflection mechanism that explicitly identifies and targets the geometric regions preventing further improvement, rather than relying on generic self-correction.

4. Results

New Lower Bound: The system successfully improved the certified lower bound of the Steiner ratio from 0.824 (Chung & Graham, 1985) to 0.8559.
Efficiency: The entire research effort required only approximately 10 iterations of the refinement loop.
Resource Usage: The process involved roughly thousands of LLM calls and consumed about 0.5 million tokens (approx. 35K per round) over 4.6 hours of reasoning time. The total computational cost was a few hundred dollars.
Robustness: Experiments using different LLM backbones (GPT-5 and Gemini 3 Pro) yielded consistent convergence to the same lower bound, demonstrating the framework's robustness to model choice.
Verification: All generated lemmas were manually checked for correctness, and the final lower bound was rigorously verified across the entire parameter space using symbolic tools (Cylindrical Algebraic Decomposition).

5. Significance and Claims

The paper claims to demonstrate the strong potential of LLM-based systems for advanced mathematical research, specifically in domains requiring deep geometric intuition and combinatorial search.

Scalability: The authors argue that their approach offers a scalable paradigm where LLMs handle creative search and lemma generation, while symbolic tools handle formal verification. This division of labor leverages the strengths of both.
Accessibility: With a total cost of only a few hundred dollars, the work suggests that LLM-assisted theoretical research is accessible to researchers without massive compute budgets.
Generalizability: The authors propose two design principles they believe transfer to other mathematical discovery problems:
1. Constructing a structured reasoning space by decomposing problems into parameterized lemmas rather than end-to-end proofs.
2. Reflecting on localized verifier failures by feeding specific bottleneck regions back to the model to guide targeted refinement.

The paper maintains modesty regarding the final result, noting that while the lower bound is significantly improved, the conjecture itself (0.866) remains unproven. Furthermore, the authors acknowledge current limitations, such as the reliance on human verification for lemma correctness and the scalability issues of symbolic verification (CAD) for higher-dimensional or more complex topologies. They suggest future work could involve formal proof assistants (e.g., Lean) to achieve fully autonomous discovery.