openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Source · Project

Cite & export
Open this versionExport record · JSONRecord detailsReport a correction

A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture

Arthur Freitas Ramos · David Barros Hulak · Ruy Jose Guerra Barretto de Queiroz

PublishedPublication date Jul 22, 2026
View project ↗

Overview

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 ↓

Passages

The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.

Passage 1 · OpenMath paraphrasePermalink

Generic path-flow model; directed graph realization; bounded_unsplittable_cost and dinitz_garg_goemans_cost_counterexample

A directed seven-vertex, nine-arc instance has fractional cost 58 and no congestion-allowed unsplittable routing of cost below 60.

Read at source ↗12 recorded uses ↓

Replaces an earlier passage. View versioned records →

Passage details

Passage ID: dinitz-garg-goemans-flow:entry:isabelle:v2

Source item: isabelle

Source record: dinitz-garg-goemans-flow:source:isabelle:v2

Replaces passage: dinitz-garg-goemans-flow:entry:isabelle:v1

Used in

Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.

Cost-preserving unsplittable flow →

Problem publication v9

The exact-cost rounding conjecture →

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

Assessment source ↗Statement v2 →

Formal declaration

Isabelle/HOL: the cost conjecture is false

Statement v2 →Inspect formal evidence ↓

Statement

Statement v2 →

Fractional cost 58 versus unsplittable cost 60 →

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

Assessment source ↗Statement v2 →

Construction

Cost obstruction in a small network

Statement v2 →

Formal declaration

Isabelle/HOL: the finite cost counterexample

Statement v2 →Inspect formal evidence ↓

Statement

Statement v2 →
Problem context · 5 citations

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.

View in problem →

History

The AFP records an Isabelle verification

View in problem →

History

Rybin announces the finite counterexample

View in problem →

Question

Cost-preserving unsplittable flow

View in problem →

Further reading

Inspect the formal statement, assumptions and reported checks.

View in problem →

Files

Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.

Formal code

Cost-counterexample Isabelle theory ↗

No OpenMath execution recorded

Exact proof source inspected. This digest identifies this file only, not a project build, theorem correspondence or independent reproduction.

Resource revision: 80985fd56a4cb63a90176bf4bfe456eaff949bfd

File checksum

SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.

7ff973cdf50586f3082fc514278e7b8a67e014170cf327bb54bb3676690a5cf7

Formal declarations

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_false

Commit 80985fd56a4cb63a90176bf4bfe456eaff949bfd

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_cost

Commit 80985fd56a4cb63a90176bf4bfe456eaff949bfd

Credits

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

AI involvement reported by the source

The AFP authors credit AI assistance for proof engineering and attribute the July counterexample announcement to Dmitry Rybin.

Versions

OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.

  1. 80985fd56a4cb63a90176bf4bfe456eaff949bfd · selectedObserved Oct 13, 2026 · used in current publications

    A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture

  2. A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture

Record details
Source ID
dinitz-garg-goemans-flow-isabelle
Record ID
dinitz-garg-goemans-flow:source:isabelle:v2
Recorded title
A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture
Revision
80985fd56a4cb63a90176bf4bfe456eaff949bfd
Observed
Oct 13, 2026
Source updated
Not recorded
Content SHA-256
Not recorded
Update method
Compare the exact source and publish a new immutable curation revision.
Identifier policy
Stable source identity with exact versioned passages.
Check interval
90 days
Rights
metadata-link
License
Original source license and document rights apply.

OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.

Source terms ↗