Open Research Index

Arthur742Ramos/dinitz-garg-goemans-counterexample-lean

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

Palomar Registrypalomar/PALOMAR-2026-08-29-000003Aug 29, 2026cs.DSscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-29-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-29-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'