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

Earlier version 2 of this page. View current →

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.

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. The source sends demands 15, 10 and 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 counterexampleDirected 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 cost: 58Allowed minimum: 60
Inspect the exact cost gap● Proved under stated assumptionsRead the surviving congestion theoremQuestion scopeCompare the larger planar allowanceQuestion scope

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

Text version

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. Inspect the exact cost gap

    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. Read the surviving congestion theorem

    Proved

    The original congestion guarantee

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

    The original congestion guarantee →

  3. Compare the larger planar 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.

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

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

None recorded

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 endpoint 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 formalized boundary.

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

Contributions

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.

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.

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