> ## Content Index
> Fetch the complete content index at: https://www.beyond-plausible.com/llms.txt
> Use this file to discover other available public pages before exploring further.

# Soap Films, a Broken Proof, and a New Record for the Steiner Ratio
- URL: https://www.beyond-plausible.com/soap-films-a-broken-proof-and-a-new-record-for-the-steiner-ratio/
- Published: 2026-09-01T16:58:58.000Z
- Updated: 2026-09-01T18:13:30.000Z
- Author: John Savva
- Tags: AI in Mathematics

[Home](https://www.beyond-plausible.com/steiner-ratio/)·[The story](https://www.beyond-plausible.com/steiner-ratio-record/)·[Paper](https://www.beyond-plausible.com/steiner-ratio-paper/)·[Verification note](https://www.beyond-plausible.com/steiner-verification-note/)·[Record note](https://www.beyond-plausible.com/steiner-record-note/)

# Introduction

For a finite set PPof points in the Euclidean plane, a *Steiner minimal tree* (SMT) is a shortest network connecting PP, where the network may introduce auxiliary vertices; a *minimum spanning tree* (MST) is a shortest network whose vertices are exactly PP. The *Steiner ratio* is ρ\=infPSMT(P)MST(P).\\rho\\;=\\; \\inf\_{P}\\; \\frac{\\mathrm{SMT}(P)}{\\mathrm{MST}(P)} .Gilbert and Pollak \[[1](#ref-GP68)\] conjectured ρ\=3/2\\rho= \\sqrt{3}/2, the value attained by the vertices of an equilateral triangle. Lower bounds progressed from 1/31/\\sqrt{3}\[[2](#ref-GH76)\] through 0.7430.743\[[3](#ref-CH78)\] and 0.80.8\[[4](#ref-DH83)\] to the Chung–Graham bound 0.8240.824\[[5](#ref-CG85)\]. Du and Hwang announced a complete proof in 1990 \[[6](#ref-DH90), [7](#ref-DH92)\]; the argument’s central reduction was later found to be unsupported, and the conjecture is regarded as open \[[8](#ref-IT12)\]. The Chung–Graham bound stood for four decades until Ke et al. \[[9](#ref-PKU26)\] established ρ≥0.8559\\rho\\ge 0.8559in 2026 by a case analysis whose leaf obligations are discharged by computer: a generator subdivides the parameter space of each local configuration into boxes and assigns each box an inequality certificate, and a checker verifies each certificate numerically.

Computer-assisted proofs of this shape have two distinguishable layers. The *certificate layer* is the finite dataset of per-box claims together with the checking procedure — objectively re-verifiable by anyone. The *lemma layer* is the human mathematics that justifies the checking rules: the geometric lemmas behind each certificate template, the correctness of the case decomposition, and (for checkers that sample only box corners) monotonicity or unimodality claims about the certified functions. For \[[9](#ref-PKU26)\] the lemma layer rests in part on computer-algebra sessions that were not published. This paper concerns the certificate layer; every statement below of the form “ρ≥x\\rho\\ge x” is to be read as conditional on the lemma layer of \[[9](#ref-PKU26)\], whose obligations we show transfer unchanged from 0.85590.8559to any target (Remark [1](#rem:uniform)).

#### Contributions.

1. **Independent verification** (§[3](#sec:verifier), §[4](#sec:audit)). A clean-room verifier — different language, different arithmetic (Arb ball arithmetic \[[10](#ref-Arb17)\] via python-flint), no shared code — confirms all 330,193,755330{,}193{,}755published records with zero certificate-layer failures, under strictly stronger semantics: all 2n2^nbox vertices are checked (the published checker, we find, visits 2n−12^{n-1}), and 28,845,10228{,}845{,}102regions are certified over their entire box, removing those regions’ dependence on the unimodality claim. To our knowledge this is the first independent replication of the 0.8559 certificate. Findings of the audit, none affecting validity, are reported in §[4.1](#sec:findings).
2. **Exact ceilings by a one-pass critical-ρ\\rhoanalysis** (§[5](#sec:ceiling)). Each certified splitting function has the form F(ρ)\=ρLT\*+(LS+−LS−)F(\\rho) = \\rho\\,L\_{T^\*}+ (L\_{S^+}\\!-\\!L\_{S^-})with LT\*≥0L\_{T^\*}\\ge 0, and no other component of the pipeline reads ρ\\rho. Hence each record has a critical value ρ\*\=min⁡vertices(LS−−LS+)/LT\*\\rho^\\ast = \\min\_{\\text{vertices}} (L\_{S^-}\\!-\\!L\_{S^+})/L\_{T^\*}, computable with certified enclosures, and the dataset’s supremal certifiable target is the minimum of ρ\*\\rho^\\astover all records — no bisection, no re-verification per probe. The published dataset’s exact ceiling is 𝟎.𝟖𝟓𝟓𝟗𝟎𝟎𝟎𝟔𝟎𝟔\\mathbf{0.8559000606}: the generator subdivides each box only until its certificate clears zero by 10−610^{-6}, so the published partition certifies its target and essentially nothing more.
3. **The record** (§[6](#sec:record)). Re-running the published generator with its target constant set to 0.8600.860(a one-line change against the pinned upstream commit) and verifying all 1,104,177,1031{,}104{,}177{,}103regenerated regions at the exact rational 43/5043/50yields ρ≥0.860\\rho\\ge 0.860at the certificate layer, with zero failures, zero invalid records, and zero inconclusive enclosures; 244,138,895244{,}138{,}895regions are certified over their entire boxes. Sampled scouting places the lemma set’s reach at ≥0.858\\ge 0.858for every case family and at 0.8660.866for d\_regular.

All code, tests, content-addressed manifests, and per-run records are available at [https://github.com/aimathpapers/Steiner\_Ratio](https://github.com/aimathpapers/Steiner%5FRatio?ref=beyond-plausible.com) and archived at [https://doi.org/10.5281/zenodo.22223485](https://doi.org/10.5281/zenodo.22223485?ref=beyond-plausible.com). The upstream repository and dataset carry no license and are not redistributed; reproduction fetches them from their public locations and verifies them against pinned SHA-256 hashes.

# The certificate framework of Ke et al.

We summarize the structure of \[[9](#ref-PKU26)\] as far as needed; the notation follows their artifact. The proof reduces the conjecture-bound question to four *case families* — two geometric configurations (`d_regular`, `d_steiner`), each split by the boundary condition f≥df \\ge dor f≤df \\le don two of its parameters. A local configuration is described by nnparameters (n\=5,6,7,8n = 5,6,7,8per case), so each case’s domain is a box in ℝn\\mathbb{R}^n, with some coordinates unbounded above.

For each case the authors fix a finite menu of *splittings*(combinatorial ways a hypothetical worst-case network could be cut and reconnected) and a menu of *lemmas* (human-proved geometric bounds on lengths of trapped components). For a splitting ssand lemma ℓ\\ell, the *splitting function* has the form Fs,ℓ(ρ;x)\=ρ⋅LT\*(x)+LS+(x)−LS−(x),\\begin{equation} \\label{eq:F} F\_{s,\\ell}(\\rho; x) \\;=\\; \\rho\\cdot L\_{T^\*}(x) \\;+\\; L\_{S^+}(x) \\;-\\; L\_{S^-}(x), \\end{equation} where LT\*L\_{T^\*}is a sum of edge lengths and lemma bounds (each non-negative), LS+L\_{S^+}prices the reconnection (a distance, a three-point Steiner length, or a lemma bound), and LS−L\_{S^-}sums deleted edge lengths. Non-positivity of Fs,ℓF\_{s,\\ell}over a parameter box certifies that no configuration in that box can violate the bound ρ\\rho. Lemma applicability is gated by side conditions on xx(never on ρ\\rho).

A generator program subdivides each case’s domain into boxes and, for each box, records a splitting and lemma under which non-positivity holds; the published dataset comprises 330,193,755330{,}193{,}755such records (Table [1](#tab:audit)). The published checker verifies each record by evaluating FFat box corner points in floating-point interval arithmetic; corner sampling is justified by an unpublished axis-wise unimodality claim (their “Shape Constraint”). Records whose box violates the subcase boundary condition are skipped by rule, as in the published checker.

# An independent verifier

Our verifier shares no code, language, or numerical library with the published stack (Julia / IntervalArithmetic.jl). It is written in Python over Arb \[[10](#ref-Arb17)\] ball arithmetic (python-flint): every quantity is carried as a rigorous enclosure, and a comparison is accepted only when it holds for *every* point of the enclosures. Three design points matter for what follows.

**Exact ρ\\rho.**The target is held as an exact rational (8559/100008559/10000, later 43/5043/50) and converted to a ball only at evaluation, at the working precision. No floating-point representation of the claim enters any decision.

**Stronger vertex semantics.** We evaluate FFat all 2n2^nfinite vertices of each box (with unbounded directions handled exactly as the published rules prescribe), escalating the working precision through a 128/256/512128/256/512\-bit ladder before recording anything but a clean pass, so enclosure width is never mistaken for a failure.

**Full-box certificates.** Where possible we additionally certify F≤0F \\le 0over the *entire* box by adaptive bisection with a bounded budget. A region so certified no longer depends on the unimodality claim at all.

The verifier is tested at two seams: a certificate-boundary suite over hand-constructed records with known outcomes, and an oracle suite that compares every lemma bound, condition, and composed FFagainst an independently written 60-digit mpmath reference at exact dyadic points (containment of the reference value in our enclosure, and agreement of branch decisions away from boundaries). The reference implementation is also embedded in self-contained “capsule” replay scripts that would accompany any defect claim; none were needed.

# Audit of the published certificate

__The published dataset (target 0.85590.8559), as verified by our stack. “Skipped” records are excluded by the published subcase rules (their checker would not evaluate them either); every skip was re-derived, not trusted. 28,845,10228{,}845{,}102of the checked regions were additionally certified over their entire box.__
| case                   | records     | pass (vertex)                         | pass (full box) | skipped |
| ---------------------- | ----------- | ------------------------------------- | --------------- | ------- |
| d\_regular, f≥df\\ge d | 1,888,501   | *all records verified; zero failures* |                 |         |
| d\_regular, f≤df\\le d | 63,466,354  |                                       |                 |         |
| d\_steiner, f≥df\\ge d | 5,402,950   |                                       |                 |         |
| d\_steiner, f≤df\\le d | 259,435,950 |                                       |                 |         |
| total                  | 330,193,755 | 265,761,575 checked                   | 64,432,180      |         |

Every record of the published dataset verifies: no failures, no invalid records, no inconclusive enclosures at any precision rung (Table [1](#tab:audit)). We regard the certificate layer of \[[9](#ref-PKU26)\] as independently confirmed — indeed strengthened, since our semantics subsume the published checker’s.

## Findings

The audit surfaced five findings, none affecting the validity of the published certificate, all relevant to anyone building on it.

1. Regenerating the dataset from the published generator source reproduces the mathematical content exactly (region bounds and identities), while canonical orderings and platform-dependent float formatting differ — regeneration is deterministic in content, not in bytes.
2. The published checker’s vertex loop indexes mask bits 1..n1..n, visiting 2n−12^{n-1}of the 2n2^nvertex assignments it documents. Our all-vertices verification shows the stronger property holds anyway.
3. Sentinel encodings differ between the published data (records excluded by subcase rules carry splitting id 00) and the current generator source (which emits −1\-1): the published dataset was not produced by the repository’s HEAD.
4. No upstream artifact was content-addressed; we published pinned SHA-256 manifests for the repository snapshot (commit `709673a8`) and every dataset file.
5. The v2 paper describes a Mathematica/CAD verification and lists interval arithmetic as future work, while the shipped artifact is a Julia interval checker — the peer-reviewable text and the actual proof artifact have diverged.

# Critical ρ\\rhoand exact ceilings

**Proposition 1**. *Fix a record (a box BB, splitting ss, lemma ℓ\\ell) admitted by the side conditions. As a function of the target, Fs,ℓ(ρ;x)\=ρ⋅LT\*(x)+(LS+−LS−)(x)F\_{s,\\ell}(\\rho; x) = \\rho \\cdot L\_{T^\*}(x) + (L\_{S^+}\\!-\\!L\_{S^-})(x)with LT\*(x)≥0L\_{T^\*}(x) \\ge 0, and neither the side conditions nor the skip rules depend on ρ\\rho. Consequently, for each checked vertex xxthe set of targets certified at xxis an interval (−∞,ρ\*(x)\](-\\infty, \\rho^\\ast(x)\](or all targets, when LT\*(x)\=0L\_{T^\*}(x)=0and (LS+−LS−)(x)≤0(L\_{S^+}\\!-\\!L\_{S^-})(x) \\le 0), with ρ\*(x)\=LS−(x)−LS+(x)LT\*(x),\\rho^\\ast(x) \\;=\\; \\frac{L\_{S^-}(x) - L\_{S^+}(x)}{L\_{T^\*}(x)},and the record’s supremal certifiable target is ρ\*(B)\=min⁡x∈V(B)ρ\*(x)\\rho^\\ast(B) = \\min\_{x \\in V(B)} \\rho^\\ast(x) over the checked vertex set V(B)V(B). The dataset’s supremal certifiable target is the minimum of ρ\*(B)\\rho^\\ast(B)over its records.*

*Proof.* Affineness and the sign of LT\*L\_{T^\*}are immediate from [\[eq:F\]](#eq:F): LT\*L\_{T^\*}is a sum of Euclidean lengths and lemma bounds, each non-negative on its admissible domain. Monotonicity of ρ↦F\\rho\\mapsto Fin ρ\\rhothen gives the interval structure at each vertex; intersecting over vertices and over records gives the minima. Since side conditions and skip rules are ρ\\rho\-free, the checked vertex set V(B)V(B)and the admitted record set are the same for every target, so the minima are well-defined independently of ρ\\rho. ◻

Ball arithmetic delivers certified two-sided enclosures of each ρ\*(B)\\rho^\\ast(B)(division of enclosures, with zero-straddling denominators handled conservatively: a certified (LS+−LS−)(x)\>0(L\_{S^+}\\!-\\!L\_{S^-})(x) > 0means the vertex fails at every target since LT\*≥0L\_{T^\*}\\ge 0; a denominator enclosure touching zero with (LS+−LS−)(x)≤0(L\_{S^+}\\!-\\!L\_{S^-})(x) \\le 0still yields a valid lower bound). One pass over the dataset therefore computes the exact ceiling. For full-box certificates the same ratio, evaluated on each leaf of the certifying subdivision, gives a one-sided bound valid over the whole box.

__Exact supremal certifiable targets of the published dataset (certified enclosure widths below 10−1010^{-10}; zero inconclusive records). The published certificate proves ρ≥0.8559\\rho\\ge 0.8559and nothing materially more.__
| case                   | records     | exact ceiling of the published partition      |
| ---------------------- | ----------- | --------------------------------------------- |
| d\_regular, f≥df\\ge d | 1,888,501   | 0.85590012790.8559001279                      |
| d\_regular, f≤df\\le d | 63,466,354  | 0.85590006190.8559000619                      |
| d\_steiner, f≥df\\ge d | 5,402,950   | 0.85590009430.8559000943                      |
| d\_steiner, f≤df\\le d | 259,435,950 | 𝟎.𝟖𝟓𝟓𝟗𝟎𝟎𝟎𝟔𝟎𝟔\\mathbf{0.8559000606} |

Table [2](#tab:ceilings) gives the result: the published dataset’s ceiling is 0.85590006060.8559000606. The explanation is a single line of the generator: each box is subdivided only until its certificate clears zero by a tolerance of 10−610^{-6}, so the partition is tailored to its target with essentially no slack. The bound 0.85590.8559was pinned by a stopping rule. This immediately suggests the experiment of the next section.

**Remark 1**. *Every lemma-layer obligation inherited from \[[9](#ref-PKU26)\] — the geometric lemmas, the case decomposition, monotonicity of constituent lengths, and the unimodality claim where vertex checking is used — is a statement about lengths and geometry in which ρ\\rhodoes not appear. The obligations therefore transfer unchanged to any target; certifying a regenerated partition at a higher ρ\\rhoincurs no new lemma-layer debt.*

# Regeneration and the record

__The record verification: partitions regenerated at target 0.8600.860, every record verified at the exact rational 43/5043/50under full-box-first semantics. SHA-256 hashes of the four certificate files are recorded in the artifact manifests.__
| case                   | records       | vertex pass | full box    | skipped    | defects |
| ---------------------- | ------------- | ----------- | ----------- | ---------- | ------- |
| d\_regular, f≥df\\ge d | 105,508,647   | 88,464,876  | 17,043,771  | 0          | 0       |
| d\_regular, f≤df\\le d | 306,908,065   | 189,196,066 | 97,215,618  | 20,496,381 | 0       |
| d\_steiner, f≤df\\le d | 291,063,158   | 231,250,637 | 46,280,442  | 13,532,079 | 0       |
| d\_steiner, f≥df\\ge d | 400,697,233   | 316,783,555 | 83,599,064  | 314,614    | 0       |
| total                  | 1,104,177,103 |             | 244,138,895 |            | **0**   |

We re-ran the published generator — from the pinned snapshot, in isolated working directories, with exactly one source change per case family: the constant `rho = 0.8559` set to the new target — and verified the regenerated partitions with the stack of §[3](#sec:verifier) at the exact rational target. As a first step, ρ\=0.856\\rho= 0.856was certified exhaustively (559,929,762559{,}929{,}762regions, zero defects). The main result is the target 0.8600.860: all 1,104,177,1031{,}104{,}177{,}103regenerated regions verify at 43/5043/50with zero failures, zero invalid records, and zero inconclusive enclosures (Table [3](#tab:record)); 244,138,895244{,}138{,}895regions carry full-box certificates. With Remark [1](#rem:uniform):

> **Certificate-layer bound.** Subject to the lemma layer of \[[9](#ref-PKU26)\], the Steiner ratio satisfies ρ≥0.860\\rho\\ge 0.860.

#### Cost.

Regeneration took between 0.90.9and 9.69.6hours per case (single-threaded, Apple M-series); partition sizes grew by factors between 1.11.1and 3232relative to the published ones. Verification throughput was ≈4,600\\approx 4{,}600records/second at 16 worker processes; the largest case verified in about two days.

#### Scouting above 0.860.

Sampled critical-ρ\\rhoanalyses (50,000 records per partition, certified per-record enclosures, zero adverse outcomes in every sample) were run on regenerated partitions at higher targets: for d\_steiner, targets 0.8570.857and 0.8580.858; for d\_regular, targets through 0.8660.866, where the sampled partition still certifies its target — within 2.5×10−52.5 \\times 10^{-5}of 3/2\\sqrt{3}/2. These are scouting results on samples, not claims; we state as claims only the exhaustively verified targets 0.8560.856and 0.8600.860.

# Scope and threats to validity

**The lemma layer is inherited, not verified.** Our result is exactly as conditional as the published one, at a higher number. The specific obligations: the geometric lemmas behind certificate templates (partly unpublished computer-algebra sessions), the completeness of the case decomposition, and, for vertex-checked regions only, the axis unimodality claim. Full-box regions (244244M of 1.11.1B at 0.8600.860) do not use unimodality.

**Partition coverage is the generator’s construction.**We verify that every emitted region certifies its inequality; that the emitted regions cover each case domain is a property of the generator’s recursive subdivision, exactly as in the published work. Our audit supports (content-identical regeneration, F1) but does not prove generator correctness.

**Trust in the toolchain.** Our verifier trusts Arb’s ball arithmetic and the Python runtime; the oracle seam (an independent 60-digit implementation) and the two-seam test suite (128 tests) are the mitigation. The verifier never trusts the generator’s arithmetic: certificates are re-derived from the record coordinates alone.

**What would falsify the claim.** A region of any regenerated partition whose splitting function is positive somewhere in its box; a demonstrated coverage gap in the generator’s subdivision; or a counterexample to an inherited lemma. The artifact includes a capsule mechanism producing a minimal, dependency-light replay script for any alleged defect.

# Future directions

The scouting data indicate the published lemma set is close to exhausted somewhere above 0.860.86; further progress will require new lemmas — new local geometry, rigorously certified, for which our infrastructure (bottleneck extraction, candidate falsification, replayable lemma certificates) is built. No finite refinement reaches 3/2\\sqrt{3}/2: the conjecture’s endgame requires a global-structure argument of exactly the kind that failed in 1990 \[[7](#ref-DH92), [8](#ref-IT12)\], and the certificate program should be seen as rigorously draining the neighborhood of that hard core. A machine-checked formalization (e.g. in Lean) of both layers is the natural terminal state for a problem with this history; the artifact’s exact-rational, replayable structure is designed to make that translation tractable.

# AI Authorship Statement

This paper, and the work it reports — the verifier implementation, the test suites, the audit, the critical-ρ\\rhoanalysis, the regeneration campaign, and the drafting of this manuscript — were carried out by Claude Fable 5, an AI system built by Anthropic, operating the computation autonomously over approximately ten days. J. Savva commissioned and directed the work, set its scope, rigor bar, and stopping decisions, provided the computing resources, reviewed the outputs, and is solely accountable for the decision to publish and for the claims made here. No mathematical statement in this paper rests on the AI’s judgment: every verification outcome is the result of certified interval arithmetic, every artifact is content-addressed, and every claim is reproducible from the public repository by the commands documented there. The mathematical machinery being verified and extended is due to the authors of \[[9](#ref-PKU26)\].

## Acknowledgments

Ke, Huang, Shu, He, Gai, and Wang \[[9](#ref-PKU26)\] built the lemma set, case decomposition, and generator on which everything here stands; this work would not exist without theirs. F. Johansson’s Arb library \[[10](#ref-Arb17)\] provides the certified arithmetic.

# References

1. E. N. Gilbert and H. O. Pollak, Steiner minimal trees, *SIAM J. Appl. Math.* 16 (1968), 1–29.
2. R. L. Graham and F. K. Hwang, Remarks on Steiner minimal trees, I, *Bull. Inst. Math. Acad. Sinica* 4 (1976), 177–182.
3. F. R. K. Chung and F. K. Hwang, A lower bound for the Steiner tree problem, *SIAM J. Appl. Math.* 34 (1978), 27–36.
4. D.-Z. Du and F. K. Hwang, A new bound for the Steiner ratio, *Trans. Amer. Math. Soc.* 278 (1983), 137–148.
5. F. R. K. Chung and R. L. Graham, A new bound for Euclidean Steiner minimal trees, *Ann. N.Y. Acad. Sci.* 440 (1985), 328–346.
6. D.-Z. Du and F. K. Hwang, The Steiner ratio conjecture of Gilbert and Pollak is true, *Proc. Natl. Acad. Sci. USA* 87 (1990), 9464–9466.
7. D.-Z. Du and F. K. Hwang, A proof of the Gilbert–Pollak conjecture on the Steiner ratio, *Algorithmica* 7 (1992), 121–135.
8. A. O. Ivanov and A. A. Tuzhilin, The Steiner ratio Gilbert–Pollak conjecture is still open, *Algorithmica* 62 (2012), 630–632.
9. Y. Ke, T. Huang, Y. Shu, D. He, J. Gai, and L. Wang, Towards solving the Gilbert–Pollak conjecture via large language models, arXiv:2601.22365 (2026), v2 May 2026, DOI 10.48550/arXiv.2601.22365; artifact: `github.com/keyisi2006/Steiner-Ratio`, pinned at commit `709673a8`.
10. F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic, *IEEE Trans. Computers* 66(8) (2017), 1281–1292.

**Artifact and reproduction:** [github.com/aimathpapers/Steiner\_Ratio](https://github.com/aimathpapers/Steiner%5FRatio?ref=beyond-plausible.com) · archived at [doi.org/10.5281/zenodo.22223485](https://doi.org/10.5281/zenodo.22223485?ref=beyond-plausible.com)

**Builds on:** Y. Ke, T. Huang, Y. Shu, D. He, J. Gai and L. Wang, *Towards Solving the Gilbert–Pollak Conjecture via Large Language Models*, [arXiv:2601.22365](https://arxiv.org/abs/2601.22365?ref=beyond-plausible.com)(2026) — the lemma set, case decomposition and partition generator used here are theirs.

**AI disclosure:** the verification software, the analysis and the drafting of these documents were carried out by an AI system (Claude Fable 5, Anthropic) working under the direction of J. Savva, who is accountable for all claims. Every mathematical claim rests on certified interval arithmetic and is reproducible from the public artifact.

Contact: [aimathpapers@gmail.com](mailto:aimathpapers@gmail.com)