HEXAGONbeta

A Lean Certificate for the Single Source Unsplittable Flow Cost Counterexample

Primarily AI-generated textHuman understanding: some partscs.DS — Data Structures and Algorithmsmath.LO — Logic

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

We explain a standalone Lean 4 and Mathlib verification of the finite counterexample announced by Dmitry Rybin to the cost-preserving single-source unsplittable-flow conjecture. The instance has seven vertices, nine directed arcs, and three terminal demands. An exact rational path flow saturates every arc, has cost 58, and has largest demand 15. Exhaustive graph-path classification reduces every unsplittable routing to two choices per terminal. Three backbone-arc inequalities force any routing with load at most the fractional load plus 15 to use at least two paid routes, each costing 30. Thus every such routing costs at least 60, ruling out cost preservation even with a non-strict congestion bound. We present the numerical certificate, its graph realization, and the boundary between the pinned proved implementation and its statement-only verification interface. The contribution is an exposition of a source-based formal certificate; no new counterexample, first formalization, or general rounding algorithm is claimed.

Provenance statement

Manuscript primarily generated with OpenAI GPT-6.1 assistance for exposition, source comparison, bibliographic research and typesetting. Arthur Freitas Ramos directed submission and reports understanding some parts. No comprehensive personal line-by-line review or complete understanding by all listed authors is claimed. Historical Lean repository metadata separately records GPT-5 agent assistance; original discovery credited to Dmitry Rybin and his GPT-5.6 Pro session. Prior AFP Isabelle formalization and separate Lean verifications by Jason Hickey and DiscreteAlias are attributed. No new counterexample, formalization priority or general algorithm claim. The source is pinned at cc7284cf415fc2a773f00d400319ef39663c277a in https://github.com/Arthur742Ramos/dinitz-garg-goemans-counterexample-lean. Exact rational certificate uses seven vertices, nine arcs, three demands 15/10/15, feasible fractional cost 58 and maximum demand 15; every weakly additive-bounded integral routing costs at least 60. Exhaustive graph path proof inspected. Challenge has seven deliberate comparator placeholders; Solution imports the proved implementation. Historical Palomar mechanical verification run 33131019615 on August 28, 2026 is distinguished from the current read-only source audit. Lean v4.33.0; Mathlib manifest db584cd6d46c92f209a44c0f1c829460d327499d. No fresh Lean build or current transitive axiom execution was performed. LaTeX PDF compiled and all pages inspected; exact source-only ZIP extracted and recompiled. Manuscript and TeX/Bib source CC BY 4.0; source code Apache-2.0; AFP BSD. Independent AI mathematical, source-alignment and bibliography review cleared the frozen manuscript on October 1, 2026; all six final pages were also independently rendered and inspected. This is not human peer review.
FormalizationsPalomar

Tools used

Lean
LeanVersion 4.33.0 (historical pinned proofs)
OpenAI
CodexVersion GPT-6.1 (manuscript)

References

  1. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021. \urlhttps://doi.org/10.1007/978-3-030-79876-5_37DOI
  2. Dinitz, Yefim; Garg, Naveen; Goemans, Michel X. On the Single-Source Unsplittable Flow Problem. Combinatorica, vol. 19, no. 1, pp. 17–41. 1999. \urlhttps://doi.org/10.1007/s004930050043DOI
  3. DiscreteAlias. unsplittable-flow. 2026. Separate verification and catalogue of cost-conjecture formulations. Repository consulted October 1, 2026. \urlhttps://github.com/DiscreteAlias/unsplittable-flow
  4. Hickey, Jason. dinitz-verify. 2026. With Claude assistance; separate verification of the same finite witness. Repository consulted October 1, 2026. \urlhttps://github.com/jyh/dinitz-verify
  5. Palomar Registry. PALOMAR-2026-08-29-000003, version 1. 2026. Registered August 29, 2026. \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-08-29-000003&version=1
  6. Ramos, Arthur Freitas; Hulak, David Barros; de Queiroz, Ruy Jose Guerra Barretto. A Formal Counterexample to the Cost-Preserving Single-Source Unsplittable Flow Conjecture. 2026. Entry dated July 22, 2026. Isabelle/HOL formalization. \urlhttps://isa-afp.org/entries/Dinitz_Garg_Goemans_Counterexample.html
  7. Ramos, Arthur Freitas; Hulak, David Barros; de Queiroz, Ruy Jose Guerra Barretto. Lean formalization of the Dinitz–Garg–Goemans cost counterexample. 2026. Revision \nolinkurlcc7284cf415fc2a773f00d400319ef39663c277a. \urlhttps://github.com/Arthur742Ramos/dinitz-garg-goemans-counterexample-lean/tree/cc7284cf415fc2a773f00d400319ef39663c277a
  8. Rybin, Dmitry. Counterexample to Dinitz Conjecture. 2026. Source discovery transcript, including the complete finite certificate. \urlhttps://chatgpt.com/share/6a60b2eb-0b64-83ee-9c76-7931ca1de063
  9. Rybin, Dmitry. Counterexample to the Dinitz–Garg–Goemans cost conjecture. 2026. \urlhttps://x.com/DmitryRybin1/status/2079904005652893709
  10. The mathlib Community. The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 367–381. 2020. \urlhttps://doi.org/10.1145/3372885.3373824DOI
  11. Traub, Vera; Vargas Koch, Laura; Zenklusen, Rico. Single-source unsplittable flows in planar and bounded-genus graphs. 2026. Published July 22, 2026. Definition 1.1 and Conjecture 1.3. \urlhttps://doi.org/10.1007/s10107-026-02365-xDOI

Version history

  1. v1Initial depositCurrentOct 01, 2026