The project verifies the rational and real cost conjecture refutations and exact optimum 60 for the displayed instance.
Public formal source; execution and statement correspondence are separate checks.
1 cited passage ↓1 problem ↓Record ffba3523f0edd14be3460d039f22a6b98c02fd9e ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
The project verifies the rational and real cost conjecture refutations and exact optimum 60 for the displayed instance.
Replaces an earlier passage. View versioned records →
Passage ID: dinitz-garg-goemans-flow:entry:lean:v2
Source item: lean
Source record: dinitz-garg-goemans-flow:source:lean:v2
Replaces passage: dinitz-garg-goemans-flow:entry:lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v9
Source assessment
Proved
Independent exact Lean verification reported
Rational and real instance; exact congestion-constrained optimum 60.
Source date Aug 1, 2026 · Observed Oct 13, 2026
Construction
Cost obstruction in a small network
Formal declaration
Lean: exact optimum 60
Formal declaration
Lean: the literature-faithful rational cost conjecture is false
Research activity
Reproduce the two formal evidence paths
The AFP theory and the Lean project expose independent definitions, path enumerations and theorem targets.
Local finite arithmetic checks are not execution of either proof assistant.
History
A pinned independent Lean verification
History
Rybin announces the finite counterexample
Question
Cost-preserving unsplittable flow
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Exact proof source inspected. This digest identifies this file only, not a project build, theorem correspondence or independent reproduction.
Resource revision: ffba3523f0edd14be3460d039f22a6b98c02fd9e
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
47aeb788d2a1487e83a2b174aee5ee79208bfb99a810c30006265dcf32504604Complete formal proof reported externally
The formal theorem establishes non-vacuity and the exact optimum. The project’s check script reports only standard logical axioms; OpenMath has not run that script.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Submission.optimum_is_sixtyCommit ffba3523f0edd14be3460d039f22a6b98c02fd9e
Complete formal proof reported externally
This declaration proves the negation of the positive conjecture above, over ℚ. Its name denotes a refutation, not a proof of the conjecture. The repository separately supplies a real-coefficient refutation. Planarity is discussed in the README and is not part of its formal statement.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Submission.goemans_cost_conjecture_falseCommit ffba3523f0edd14be3460d039f22a6b98c02fd9e
Recorded authorship
Jason Hickey
Jason Hickey credits Claude for the verification work and credits Dmitry Rybin’s GPT-5.6 Pro session for the original counterexample.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Independent Lean verification of Goemans’ cost counterexample
Independent Lean verification of Goemans’ cost counterexample
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Source terms ↗