Reading source record 80985fd56a4cb63a90176bf4bfe456eaff949bfd. This record is retained from earlier public citations. View default cited record →
A directed seven-vertex, nine-arc instance has fractional cost 58 and no congestion-allowed unsplittable routing of cost below 60.
Public formal source; execution and statement correspondence are separate checks.
1 cited passage ↓1 problem ↓Record 80985fd56a4cb63a90176bf4bfe456eaff949bfd ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
A directed seven-vertex, nine-arc instance has fractional cost 58 and no congestion-allowed unsplittable routing of cost below 60.
Passage ID: dinitz-garg-goemans-flow:entry:isabelle:v1
Source item: isabelle
Source record: dinitz-garg-goemans-flow:source:isabelle:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v3
Source assessment
Proved
Seven-vertex cost gap formally verified
Fractional cost 58; maximum demand 15; allowed unsplittable cost at least 60.
Source date Jul 22, 2026 · Observed Oct 13, 2026
Formal declaration
Isabelle/HOL: the finite cost counterexample
Source assessment
Disproved
Cost-preserving rounding conjecture refuted
The conjunction of a largest-demand congestion allowance and preservation of fractional cost.
Source date Jul 22, 2026 · Observed Oct 13, 2026
Formal declaration
Isabelle/HOL: the cost conjecture is false
Research activity
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.
History
Rybin announces the finite counterexample
History
The AFP records an Isabelle verification
Question
Cost-preserving unsplittable flow
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Resource revision: 80985fd56a4cb63a90176bf4bfe456eaff949bfd
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
7ff973cdf50586f3082fc514278e7b8a67e014170cf327bb54bb3676690a5cf7Complete 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 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
Recorded authorship
Arthur Freitas Ramos · David Barros Hulak · Ruy Jose Guerra Barretto de Queiroz
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.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Source terms ↗