{"id":"palomar/PALOMAR-2026-08-29-000003","url":"https://github.com/Arthur742Ramos/dinitz-garg-goemans-counterexample-lean/tree/cc7284cf415fc2a773f00d400319ef39663c277a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000003-v1.json","repo":"https://github.com/Arthur742Ramos/dinitz-garg-goemans-counterexample-lean","tags":["cs.DS","math.LO","msc:68R10","msc:90C27","msc:03B35","combinatorial-optimization","lean-formalization","unsplittable-flow","network-flows"],"score":0,"title":"Arthur742Ramos/dinitz-garg-goemans-counterexample-lean","trust":"high","domain":"cs.DS","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"cs.DS","summary":"A standalone Lean 4 and Mathlib formalization of the finite counterexample to the cost-preserving single-source unsplittable-flow conjecture. The development realizes a directed graph with seven vertices, nine arcs, and three terminal demands; checks a feasible rational fractional flow of cost 58 with maximum demand 15; and proves that every unsplittable routing under the weak additive congestion bound has cost at least 60. It also derives the failure of the strict congestion variant. No general algorithmic or complexity-theoretic claim is made.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-08-29","reactions":{},"formalized":true}