Combinatorial optimization · Graph theory · Conjecture
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?
Earlier version 6 of this page. View current →
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.
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.
Question paraphrased by OpenMath. Original wording is available in the sources.
Figures and explorable examples. Selecting a statement opens its exact wording.
Visual setup
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.
Each arrow follows the directed network. Labels are load / unit cost; the full text view lists every arc.
Goemans’ cost-enhanced assertion is refuted; the original congestion-only theorem is not.
Conjecture · Primary formulation
DisprovedRamos et al. 2026The exact-cost rounding conjecture
Goemans’ cost-enhanced assertion is refuted; the original congestion-only theorem is not.
A finite exhaustive path-choice witness. The source contains four capacity-allowed routings, so the cost gap is not vacuous.
Theorem · Counterexample
ProvedRamos et al. 2026Fractional 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.
Traub–Vargas Koch–Zenklusen’s planar theorem has a larger allowance and therefore survives the counterexample.
Theorem · Different statement · related variant
ProvedTraub et al. 2023Preserving cost with twice the allowance in planar graphs
Traub–Vargas Koch–Zenklusen’s planar theorem has a larger allowance and therefore survives the counterexample.
Dinitz–Garg–Goemans’ theorem provides congestion control without promising the same cost.
Theorem · Supporting result
ProvedTraub et al. 2023The original congestion guarantee
Dinitz–Garg–Goemans’ theorem provides congestion control without promising the same cost.
The schematic shows the idea. The exact arc data, fractional routing and path enumeration are in the linked Isabelle and Lean sources; this summary is not an executed network certificate.
Fractional cost 58 versus unsplittable cost 60 →Assuming Fractional cost 58 versus unsplittable cost 60Proved
Congestion control and cost control do not combine for free
Under stated assumptionsThe witness separates preserving the fractional cost from the valid largest-demand congestion guarantee. Algorithmic guarantees must state both allowances precisely.
Limit It does not refute the original theorem or the planar 2 d_max cost theorem.
Supporting statements
Source-grounded explanation · independent explanation review: pending.
How the problem is attacked, and what each line of attack cannot yet reach.
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.
Supporting statements
Source-grounded explanation · independent explanation review: pending.
Jason Hickey’s project checks the exact optimum and the literature-faithful conjecture refutation.
This is a source-reported verification, not an OpenMath build.
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.
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.
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.
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.
| Literature | 1 published paper · 1 preprint · 1 project Status OpenMath assessment · Oct 13, 2026.
|
|---|---|
| Formal | 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 | |
| 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. |
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
Dinitz_Garg_Goemans_Counterexample.bounded_unsplittable_costCommit 80985fd56a4cb63a90176bf4bfe456eaff949bfd
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
Submission.optimum_is_sixtyCommit ffba3523f0edd14be3460d039f22a6b98c02fd9e
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
Dinitz_Garg_Goemans_Counterexample.weak_dgg_cost_conjecture_falseCommit 80985fd56a4cb63a90176bf4bfe456eaff949bfd
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
Submission.goemans_cost_conjecture_falseCommit ffba3523f0edd14be3460d039f22a6b98c02fd9e
External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.
Choose a starting point below. Each result links to its exact statement, cited passages and checks.
Consult the original question and its hypotheses.
Inspect the formal statement, assumptions and reported checks.
Inspect the formal statement, assumptions and reported checks.
Vera Traub · Laura Vargas Koch · Rico Zenklusen · Preprint · Aug 4, 2023
Definition 1.1, Theorem 1.2, Conjecture 1.3 and Theorem 1.8
Arthur Freitas Ramos · David Barros Hulak · Ruy Jose Guerra Barretto de Queiroz · Published · Jul 22, 2026
Generic path-flow model; directed graph realization; bounded_unsplittable_cost and dinitz_garg_goemans_cost_counterexample
Jason Hickey · Project documentation · Aug 1, 2026
Submission.lean headline theorems; README provenance and verification boundaries
Formalization
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
Independent Lean verification of Goemans’ cost counterexample · sources & artifacts →
Selected literature; source observations and coverage limits are retained in the publication details.
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.
Vera Traub · Laura Vargas Koch · Rico Zenklusen
No specific AI contribution is attributed by this source record.
Arthur Freitas Ramos · David Barros Hulak · Ruy Jose Guerra Barretto de Queiroz
The AFP authors credit AI assistance for proof engineering and attribute the July counterexample announcement to Dmitry Rybin.
Jason Hickey
Jason Hickey credits Claude for the verification work and credits Dmitry Rybin’s GPT-5.6 Pro session for the original counterexample.
These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.