Formally verified AI-led

Counterexample to the Dinitz–Garg–Goemans conjecture

An explicit seven-node network whose cheapest single-route (unsplittable) shipping costs more than its fractional cost even under the allowed capacity slack, disproving a conjecture from the late 1990s.

Lab: Independent
Model: GPT-5.6 Pro
Field: Computer science
Date: 2026-07-22
Human collaborators: Dmitry Rybin
Problem posed: 1999 · open 27 yrs

Sources

What was found

Dinitz, Garg, and Goemans proved that any fractional multicommodity flow can be rounded to an unsplittable (single-path-per-demand) flow while violating each arc's capacity by at most the maximum demand. Goemans conjectured this rounding could also be done without increasing the total cost. The counterexample is a directed graph on seven nodes carrying three demands (15, 10, 15); its fractional solution costs 58, yet every unsplittable routing that stays within the allowed capacity cushion (violation $\le 15$ ) costs at least 60. Rybin reached it with GPT-5.6 Pro in four short prompts and reported that the model returned proof certificates, an exhaustive-enumeration verification program, machine-readable data, and LaTeX source.

Novelty check

The Dinitz–Garg–Goemans unsplittable-flow result is from the late 1990s (D. Dinitz, N. Garg, M. Goemans, 'On the single-source unsplittable flow problem'); the cost-preserving strengthening was an open conjecture attributed to Goemans. No prior counterexample or resolution appears in the literature. The construction is a new concrete instance, not a retrieval of an existing example.

Caveats and known objections

Not peer-reviewed. The counterexample was shared on X with a public GPT-5.6 Pro transcript rather than in a paper, and the entry was downgraded from author verified to claimed on 2026-08-02 because no standalone artifact was linked. That gap has since been closed by people other than the author: an Archive of Formal Proofs entry by Arthur Freitas Ramos, David Barros Hulak and Ruy de Queiroz formalizes the seven-vertex instance in Isabelle and proves that no unsplittable routing within the allowed congestion matches the fractional cost, which is the whole content of a finite counterexample, so the grade is formal. The formalization uses its own finite path-flow model of the problem, and its authors disclose AI assistance with the proof engineering. Hensen Juang publicly generalized the instance into an infinite parametric family on the same seven nodes, which is consistent with the claim. Autonomy graded ai-led: the model produced the construction; the human posed the problem and verified.

Independent checks

Arthur Freitas Ramos, David Barros Hulak and Ruy J. G. B. de Queiroz (Archive of Formal Proofs): Formalized the seven-vertex, nine-arc instance in Isabelle/HOL and proved that its fractional flow of cost 58 cannot be rounded to any unsplittable routing that keeps the cost, even under the non-strict congestion allowance of $d_{\max} = 15$ . AI assistance was used for proof engineering; Isabelle checks the final statements and proofs. · link ↗

The open problem

MathDBDinitz–Garg–Goemans conjecture

316187

Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.

Also recorded at

vibematheddinitz-garg-goemans-unsplittable-flow

Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

History of this entry

2026-09-24RegradedUpgraded from claimed to formally verified: an Archive of Formal Proofs entry by three authors unconnected to the announcement machine-checks the counterexample in Isabelle, supplying the standalone artifact whose absence caused the August downgrade. source ↗
2026-08-21CorrectedRecorded the vibemathed record for this result as a registration. It sits alongside the MathDB record already cited. No grade moved.
2026-08-19CorrectedRecorded the MathDB record for this result as a registration.
2026-08-02RegradedDowngraded from author verified to claimed: classifying the sources showed no primary artifact, only a chat transcript.
2026-07-24AddedEntered the registry graded Formally verified and AI-led.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Community discussion

XHensen Juang: infinite family generalizing the counterexample (X)↗

Graded formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Counterexample to the Dinitz–Garg–Goemans conjecture. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-22-dinitz-garg-goemans

BibTeX

@misc{whataifound-independent-2026-goemans,
  title        = {Counterexample to the Dinitz–Garg–Goemans conjecture},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-07-22-dinitz-garg-goemans}
}

Related findings

ClaimedCounterexamples to Zak's modified integer round-down conjecture for the skiving stock problemIndependent · 2026-10-07 Formally verifiedSix-task counterexample to the Kernel Conjecture of pinwheel schedulingIndependent · 2026-09-30 Author verifiedMarton's inner bound shown not to reach the broadcast channel capacity regionIndependent · 2026-08-20

combinatorial-optimization network-flow counterexample unsplittable-flow

← All computer science findings in the registry