Algorithm A computes the length of the Steiner tree connecting $Y$

Proved

DreyfusWagner.Steiner.algorithmA_eq_steinerLength

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-programminggraph-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1steiner-tree

Let $G = (N, A)$ be a finite connected undirected graph whose arcs have positive lengths, with the node set $N$ linearly ordered in any way. Let $Y \subseteq N$ contain at least three nodes and let $q \in Y$ . Then the value $v$ returned by Algorithm A of Dreyfus and Wagner (with $C = Y - \{q\}$ and the shortest-path lengths $D(i,j)$ of $G$ as input) is the length of the Steiner tree connecting $Y$ :

v = \operatorname{St}(Y) = \min\{\, |S| : S \subseteq A,\ S \text{ connects } Y \,\}.

This is the main result of the paper: the Dreyfus–Wagner dynamic program solves the Steiner problem in graphs exactly, in time exponential only in the number of terminals.

Formalization Note The hypothesis $\|Y\| \ge 3$ is the paper's own (Appendix A, p. 205). For $\|Y\| = 2$ Algorithm A as printed returns $+\infty$ (line (18) admits no set $E$ ), and the two-node case is covered by the shortest path instead. The order on $N$ is arbitrary: the conclusion holds for every choice of $A[1]$ . Values are in WithTop ℝ; under the hypotheses both sides are finite.

Preamble

import Mathlib
import Definitions.Def_DreyfusWagner_Steiner_SteinerProblem
import Definitions.Def_DreyfusWagner_Steiner_AlgorithmA

Formal statement

namespace DreyfusWagner.Steiner

/-- Dreyfus–Wagner 1971, §4, Algorithm A, p. 203: for a finite connected undirected graph with
positive arc lengths, a set `Y` of at least three nodes and any `q ∈ Y`, Algorithm A returns
the length of the Steiner tree connecting `Y`, whatever the order of the nodes. -/
theorem algorithmA_eq_steinerLength {V : Type*} [Fintype V] [LinearOrder V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (ℓ : Sym2 V → ℝ)
    (hpos : ∀ e ∈ G.edgeSet, 0 < ℓ e) (hconn : G.Connected)
    (Y : Finset V) (hY : 3 ≤ Y.card) (q : V) (hq : q ∈ Y) :
    algorithmA G ℓ Y q = steinerLength G ℓ Y := by sorry

end DreyfusWagner.Steiner

Source

Dreyfus, Wagner, The Steiner Problem in Graphs, Networks 1 (1971), p. 203, §4, Algorithm A (caption: 'Computes the length of the Steiner tree connecting Y'); Abstract, p. 195; hypothesis ‖Y‖ ≥ 3 from Appendix A, p. 205

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $V$ be any finite type of vertices with any linear order $\le$ on it. The statement holds for every such order, so neither side is claimed to depend on which order is chosen. Let $G$ be a simple graph on $V$ : undirected, with no loops and no multiple edges, and with decidable adjacency. Let

\ell : \{\text{unordered pairs } \{u,v\} \text{ of vertices}\} \to \mathbb{R}

be a real-valued length function. It is defined on all unordered pairs, including non-adjacent pairs and "diagonal" pairs $\{v,v\}$ , not only on the edges of $G$ .

The hypotheses are:

(positivity) $\ell(e) > 0$ for every edge $e$ of $G$ . No condition is placed on $\ell$ at pairs that are not edges, so there it may be zero, negative or anything else.
(connectivity) $G$ is connected. In particular $V$ is non-empty, and any two vertices are joined by a path in $G$ .
(terminals) $Y$ is a finite set of vertices with $|Y| \ge 3$ .
(root) $q$ is a vertex with $q \in Y$ .

The conclusion is the equation

\mathrm{algorithmA}(G, \ell, Y, q) \;=\; \mathrm{steinerLength}(G, \ell, Y).

Here $\mathrm{algorithmA}$ is a function of the graph, the length function, the terminal set and the chosen terminal $q$ . $\mathrm{steinerLength}$ is a function of the graph, the length function and the terminal set only. Both are defined in the imported files Def_DreyfusWagner_Steiner_AlgorithmA and Def_DreyfusWagner_Steiner_SteinerProblem. Their definitions are not part of the code I was given, so I cannot spell out what they compute or what type of value they return. The documentation comment calls them "Algorithm A" of Dreyfus–Wagner and "the length of the Steiner tree connecting $Y$ ", but that is only a comment, not something the code asserts. Because the equation holds for every $q \in Y$ , it also implies that the left-hand side has the same value for every choice of terminal $q$ .

Degenerate cases:

Size of $V$ and $Y$ : Since $|Y| \ge 3$ , $V$ has at least three elements. The empty type, a one-element type and a two-element type are therefore excluded, and so are terminal sets with 0, 1 or 2 elements; the statement says nothing about them.
Vacuity: The hypotheses can all be satisfied, so the statement is not vacuous. For example, take a triangle with all three edge lengths equal to $1$ , $Y$ equal to all three vertices, and any $q \in Y$ .
Lengths off the edges: The values of $\ell$ on non-edges and on diagonal pairs $\{v,v\}$ are completely unconstrained. Those pairs are never edges of a simple graph. The equation is claimed for every such choice of those values. Whether either side actually reads them depends on the definitions I cannot see.
Default values: Any default or "junk" value those definitions might produce is also outside what I can see. Examples are a minimum or infimum over an empty family, or a sum over no terms. Whatever such values are, the statement asserts the two sides agree under the hypotheses above.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Algorithm A computes the length of the Steiner tree connecting YYY

Algorithm A computes the length of the Steiner tree connecting $Y$