openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance
← Problems

Combinatorial optimization · Graph theory · Conjecture

Cost-preserving unsplittable flow

Can a fractional single-source flow be rounded to one path per terminal without increasing cost, while increasing each arc load by at most the largest demand?

DisprovedOpenMath assessment · Oct 13, 2026
Frontier 1 report →
Cite & export
Open this versionExport record · JSONRecord detailsReport a correction
Use with an agent

Overview

Known

The exact-cost strengthening is refuted by a finite witness in the cited Isabelle and Lean sources. Congestion-only rounding and the planar doubled-allowance theorem remain valid.

Latest

Precise statement

A finite directed network has one source, terminal demands, nonnegative rational arc capacities and costs, and a feasible fractional flow x. An unsplittable routing sends each terminal’s entire demand on a single source-to-terminal path. The allowance is load(a) ≤ x(a) + d_max; it is measured against fractional load, not an arbitrary extra capacity.

Definitions

Unsplittable routing
Each terminal’s entire demand travels on one path from the source. A fractional routing may split that demand between paths.

Background

Question paraphrased by OpenMath. Original wording is available in the sources.

Landscape

Figures and explorable examples. Selecting a statement opens its exact wording.

Visual setup

The seven-node cost counterexample

Arrow labels give fractional load / cost per unit. Terminal demands are t1: 15, t2: 10 and t3: 15; d_max = 15. Every arc capacity equals its fractional load.

Reading boundary. Layout is schematic. Arrow lengths do not encode capacities, and the diagram is not an executed formal certificate.

The seven-node cost counterexampleTerminal demands are t1: 15, t2: 10 and t3: 15. Directed arcs are s→t1, s→t2, s→u, u→t3, u→v, v→t1, v→w, w→t2 and w→t3. Their fractional loads are 10, 6, 24, 10, 14, 5, 9, 4 and 5. Only s→t1, s→t2 and u→t3 have nonzero per-unit costs: 2, 3 and 2. The fractional cost is 58. The minimum unsplittable cost with additive allowance 15 is 60.suvwt1t2t310 / 26 / 324 / 010 / 214 / 05 / 09 / 04 / 05 / 0Fractional: 58Minimum: 60
Cost gap: 58 fractional, 60 unsplittable● Proved under stated assumptionsCongestion-only rounding still holdsQuestion scopePlanar variant: 2·d_max allowanceQuestion scope

Each arrow follows the directed network. Labels are load / unit cost; the full text view lists every arc.

Text version

Terminal demands are t1: 15, t2: 10 and t3: 15. Directed arcs are s→t1, s→t2, s→u, u→t3, u→v, v→t1, v→w, w→t2 and w→t3. Their fractional loads are 10, 6, 24, 10, 14, 5, 9, 4 and 5. Only s→t1, s→t2 and u→t3 have nonzero per-unit costs: 2, 3 and 2. The fractional cost is 58. The minimum unsplittable cost with additive allowance 15 is 60.

The rational network and all labels are taken from the pinned formal sources. Arcs are directed; coordinates carry no mathematical scale.

  1. Cost gap: 58 fractional, 60 unsplittable

    Proved

    Fractional cost 58 versus unsplittable cost 60

    A finite exhaustive path-choice witness. The source contains four capacity-allowed routings, so the cost gap is not vacuous.

    Fractional cost 58 versus unsplittable cost 60 →

  2. Congestion-only rounding still holds

    Proved

    The original congestion guarantee

    Dinitz–Garg–Goemans’ theorem provides congestion control without promising the same cost.

    The original congestion guarantee →

  3. Planar variant: 2·d_max allowance

    Proved

    Preserving cost with twice the allowance in planar graphs

    Traub–Vargas Koch–Zenklusen’s planar theorem has a larger allowance and therefore survives the counterexample.

    Preserving cost with twice the allowance in planar graphs →

Sources & review

Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Cost obstruction in a small network

Inspect a routing

7 vertices and 9 arcs. Each demand takes one complete path. The fractional routing costs 58; the allowed extra load on each arc is 15.

The minimum cost among allowed path combinations is 60.

Routing cost: 60. Within every arc’s load allowance.

Arc loads and costs for this routing
ArcFractional loadSelected load / limitUnit cost / cost
s → t11015 / 252 / 30
s → t2610 / 213 / 30
s → u2415 / 390 / 0
u → t3100 / 252 / 0
u → v1415 / 290 / 0
v → t150 / 200 / 0
v → w915 / 240 / 0
w → t240 / 190 / 0
w → t3515 / 200 / 0
All 8 path combinations & the fractional split
All path combinations
PathsCostLoad allowance

s → t1; s → t2; s → u → t3

90Allowed

s → t1; s → t2; s → u → v → w → t3

60Allowed

s → t1; s → u → v → w → t2; s → u → t3

60Allowed

s → t1; s → u → v → w → t2; s → u → v → w → t3

30Exceeded

s → u → v → t1; s → t2; s → u → t3

60Allowed

s → u → v → t1; s → t2; s → u → v → w → t3

30Exceeded

s → u → v → t1; s → u → v → w → t2; s → u → t3

30Exceeded

s → u → v → t1; s → u → v → w → t2; s → u → v → w → t3

0Exceeded

t1: 10 units along s → t1; 5 units along s → u → v → t1.

t2: 6 units along s → t2; 4 units along s → u → v → w → t2.

t3: 10 units along s → u → t3; 5 units along s → u → v → w → t3.

Arithmetic from the cited finite network. This explorer is not an execution of the external Isabelle or Lean proofs.

Construction details and sources ↓

Results

The question 1

Counterexamples 1

Variants and analogues 1

  • Proved
    Preserving cost with twice the allowance in planar graphs

    Traub–Vargas Koch–Zenklusen’s planar theorem has a larger allowance and therefore survives the counterexample.

    Traub et al. 2023

Background 1

  • Proved
    The original congestion guarantee

    Dinitz–Garg–Goemans’ theorem provides congestion control without promising the same cost.

    Traub et al. 2023
Constructions · 1

Connections

Consequences 1

Assuming Fractional cost 58 versus unsplittable cost 60Proved

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

Enumerate every path choice

Each of the three demands has two source-to-terminal paths, leaving eight unsplittable choices. The allowed choices all pay for at least two routes.

Cannot yet reach The finite enumeration concerns this witness; it is not a general rounding algorithm.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Timeline

  1. A pinned independent Lean verificationFormalization

    Jason Hickey’s project checks the exact optimum and the literature-faithful conjecture refutation.

    This is a source-reported verification, not an OpenMath build.

  2. Rybin announces the finite counterexampleRelated result

    The verification projects attribute the discovery to Dmitry Rybin’s GPT-5.6 Pro session.

    The original discovery and subsequent formal checks are separate contributions.

    Also on the Frontier: Dinitz–Garg–Goemans flow conjecture

  3. The AFP records an Isabelle verificationFormalization

    Ramos, Hulak and de Queiroz supply the generic flow model and exhaustive finite argument.

    The AFP entry date is distinct from the generated document’s August revision date.

  4. A planar theorem preserves cost with a larger allowanceRelated result

    Traub, Vargas Koch and Zenklusen prove the cost guarantee with two-sided deviation at most twice the largest demand.

    The larger allowance is essential to distinguishing this theorem from the refuted question.

  5. The original congestion theoremRelated result

    Dinitz, Garg and Goemans establish additive congestion bounded by the largest demand.

    The folklore cost strengthening is a separate assertion, later stated as Conjecture 1.3 in the 2023 paper.

Full history with sources →

Evidence

Literature

1 published paper · 1 preprint · 1 project

Status OpenMath assessment · Oct 13, 2026.

Formal

4 complete proofs

4 formalizations below ↓

Reported in sources: Pinned Isabelle/HOL and Lean sources report complete finite-witness checks. They have separate theorem targets and provenance. No OpenMath execution of either project is recorded.

Computation

1 explicit witness

Review

Not yet reviewed

OpenMath assessment: The exact-cost strengthening is refuted by a finite witness in the cited Isabelle and Lean sources. Congestion-only rounding and the planar doubled-allowance theorem remain valid.

Source comparison and reader curation; independent mathematical assessment remains pending.

OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027

Collection last checked Oct 13, 2026.

Formalizations

Fractional cost 58 versus unsplittable cost 60 →

Isabelle/HOL: the finite cost counterexampleComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

This exact lower-bound endpoint is combined with the theory’s explicit graph realization, fractional feasibility and cost-58 lemmas. It proves a cost of at least 60 under the non-strict additive allowance, rather than by itself specifying the full network. It is an Isabelle/HOL artifact, not a Lean theorem.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision
Dinitz_Garg_Goemans_Counterexample.bounded_unsplittable_cost

Commit 80985fd56a4cb63a90176bf4bfe456eaff949bfd

Lean: exact optimum 60Complete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

The formal theorem establishes non-vacuity and the exact optimum. The project’s check script reports only standard logical axioms; OpenMath has not run that script.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision
Submission.optimum_is_sixty

Commit ffba3523f0edd14be3460d039f22a6b98c02fd9e

The exact-cost rounding conjecture →

Isabelle/HOL: the cost conjecture is falseComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

The finite path-flow model is realized as the directed network earlier in the theory. This corollary proves the negation of cost-preserving rounding with the non-strict largest-demand allowance; it does not prove the positive conjecture.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision
Dinitz_Garg_Goemans_Counterexample.weak_dgg_cost_conjecture_false

Commit 80985fd56a4cb63a90176bf4bfe456eaff949bfd

Lean: the literature-faithful rational cost conjecture is falseComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

This declaration proves the negation of the positive conjecture above, over ℚ. Its name denotes a refutation, not a proof of the conjecture. The repository separately supplies a real-coefficient refutation. Planarity is discussed in the README and is not part of its formal statement.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision
Submission.goemans_cost_conjecture_false

Commit ffba3523f0edd14be3460d039f22a6b98c02fd9e

External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Bibliography 3

Research activity · 1 entry

Formalization

Reproduce the two formal evidence paths

The AFP theory and the Lean project expose independent definitions, path enumerations and theorem targets.

Local finite arithmetic checks are not execution of either proof assistant.

Related statements · context, not additional proved progress

A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture · sources & artifacts →

Independent Lean verification of Goemans’ cost counterexample · sources & artifacts →

Selected literature; source observations and coverage limits are retained in the publication details.

Contributors

Dmitry Rybin and his GPT-5.6 Pro session receive discovery credit, as reported by the verification sources. Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz authored the Isabelle verification. Jason Hickey, with Claude, authored the separate Lean verification. Dinitz, Garg and Goemans proved the older congestion theorem; Traub, Vargas Koch and Zenklusen supplied the later precise cost formulation and planar theorem.

Authors & roles

These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.

Record details
Record version
9
Classification
MSC2020 90C35 / 05C21
Prerequisite level
graduate
Source observations & version history →