Proved
Seven-vertex cost gap formally verified ↗
Fractional cost 58; maximum demand 15; allowed unsplittable cost at least 60.
Source dated Jul 22, 2026 · Observed Oct 13, 2026
Theorem · version 1
Fractional cost 58 versus unsplittable cost 60
Earlier version 1. View current version 2 →
Statement
There is a seven-vertex, nine-arc directed single-source network with demands 15, 10 and 15 and a feasible fractional flow of cost 58 such that every unsplittable routing satisfying load_P(a) ≤ x(a) + 15 on every arc costs at least 60.
Assumptions
- The exact rational network and costs specified in the cited formal sources.
- Non-strict upper congestion allowance measured from the fractional arc load.
Scope
A finite exhaustive path-choice witness. The source contains four capacity-allowed routings, so the cost gap is not vacuous.
Evidence
Source reports
Proved
Independent exact Lean verification reported ↗
Rational and real instance; exact congestion-constrained optimum 60.
Source dated Aug 1, 2026 · Observed Oct 13, 2026
Formal proofs
Isabelle/HOL: the finite cost counterexample ↗
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_costCommit 80985fd56a4cb63a90176bf4bfe456eaff949bfd
Lean: exact optimum 60 ↗
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_sixtyCommit ffba3523f0edd14be3460d039f22a6b98c02fd9e
Connections
In this problem · publication v2 · Selected context
Cost-preserving unsplittable flow →
Counterexample · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v3
Cost-preserving unsplittable flow →
Counterexample · Proved
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.
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 · 2
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Independent exact Lean verification reported ↗
Rational and real instance; exact congestion-constrained optimum 60.
Source dated Aug 1, 2026 · Observed Oct 13, 2026 · Source passage →
Proved
Seven-vertex cost gap formally verified ↗
Fractional cost 58; maximum demand 15; allowed unsplittable cost at least 60.
Source dated Jul 22, 2026 · Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-flow-seven-vertex-counterexample
- Statement version
- 1
- SHA-256
- 68bd01ebc842753e2ece649614ee64a27096c41d351c622572adac7a051e4928