{"id":"hexagon/2610.00009","pdf":"https://hexagonmath.org/pdf/2610.00009v1","url":"https://hexagonmath.org/abs/2610.00009v1","tags":["math.LO","msc:68R10","msc:90C27","msc:03B35","Goemans cost conjecture","Lean 4","Mathlib","Rybin counterexample","finite counterexample","formal verification"],"score":0,"title":"A Lean Certificate for the Single Source Unsplittable Flow Cost Counterexample","domain":"cs.DS","origin":"ai-generated","source":"hexagon","authors":["Arthur","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"cs.DS","summary":"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.…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"ai_models":["Codex"],"discussed":0,"published":"2026-10-01","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":true,"formalizations":["https://palomar-registry.org/entry?id=PALOMAR-2026-08-29-000003&version=1"],"human_understanding":"some"}