Disproved
Cost-preserving rounding conjecture refuted ↗
The conjunction of a largest-demand congestion allowance and preservation of fractional cost.
Source dated Jul 22, 2026 · Observed Oct 13, 2026
Conjecture · version 1
The exact-cost rounding conjecture
Earlier version 1. View current version 2 →
Statement
Every feasible fractional single-source flow x with nonnegative rational costs admits an unsplittable routing P with load_P(a) ≤ x(a) + d_max on every arc and total cost at most the cost of x.
Assumptions
- Finite directed network; feasible single-source flow and nonnegative rational capacities/costs.
- Each terminal demand is positive and must be sent along one path.
- d_max is the largest terminal demand.
Scope
Goemans’ cost-enhanced assertion is refuted; the original congestion-only theorem is not.
Evidence
Source reports
Formal proofs
Isabelle/HOL: the cost conjecture is false ↗
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_falseCommit 80985fd56a4cb63a90176bf4bfe456eaff949bfd
Lean: the literature-faithful rational cost conjecture is false ↗
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_falseCommit ffba3523f0edd14be3460d039f22a6b98c02fd9e
Connections
In this problem · publication v2 · Selected context
Cost-preserving unsplittable flow →
Primary formulation · Disproved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v3
Cost-preserving unsplittable flow →
Primary formulation · Disproved
Relationship not independently reviewed. This concerns its use in this problem.
Sources
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture →
- Generic path-flow model; directed graph realization; bounded_unsplittable_cost and dinitz_garg_goemans_cost_counterexample → · Original passage ↗
Recorded wording
A directed seven-vertex, nine-arc instance has fractional cost 58 and no congestion-allowed unsplittable routing of cost below 60.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Arthur Freitas Ramos · David Barros Hulak · Ruy Jose Guerra Barretto de Queiroz · Published · Publication date Jul 22, 2026
Public formal source; execution and statement correspondence are separate checks.
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture — pinned source ↗No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Revision & attribution
Source revision: 80985fd56a4cb63a90176bf4bfe456eaff949bfd. Observed Oct 13, 2026.
The AFP authors credit AI assistance for proof engineering and attribute the July counterexample announcement to Dmitry Rybin.
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture — pinned source: 80985fd56a4cb63a90176bf4bfe456eaff949bfd.
Independent Lean verification of Goemans’ cost counterexample →
- Submission.lean headline theorems; README provenance and verification boundaries → · Original passage ↗
Recorded wording
The project verifies the rational and real cost conjecture refutations and exact optimum 60 for the displayed instance.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Jason Hickey · Project documentation · Publication date Aug 1, 2026
Public formal source; execution and statement correspondence are separate checks.
Independent Lean verification of Goemans’ cost counterexample — pinned source ↗No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Revision & attribution
Source revision: ffba3523f0edd14be3460d039f22a6b98c02fd9e. Observed Oct 13, 2026.
Jason Hickey credits Claude for the verification work and credits Dmitry Rybin’s GPT-5.6 Pro session for the original counterexample.
Independent Lean verification of Goemans’ cost counterexample — pinned source: ffba3523f0edd14be3460d039f22a6b98c02fd9e.
Single-Source Unsplittable Flows in Planar Graphs →
- Definition 1.1, Theorem 1.2, Conjecture 1.3 and Theorem 1.8 → · Original passage ↗
Recorded wording
The paper states the original congestion theorem, Goemans’ cost-enhanced conjecture and a planar theorem with twice the largest-demand allowance.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Vera Traub · Laura Vargas Koch · Rico Zenklusen · Preprint · Publication date Aug 4, 2023
Revision & attribution
Source revision: 2023-08-04. Observed Oct 13, 2026.
No specific AI contribution is attributed by this source record.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Disproved
Cost-preserving rounding conjecture refuted ↗
The conjunction of a largest-demand congestion allowance and preservation of fractional cost.
Source dated Jul 22, 2026 · Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-flow-cost-preserving-rounding
- Statement version
- 1
- SHA-256
- d70cf94d635b8391d1183a429e4d444488464a0467dcd3d67e4c24ac5d2bfe34