Reading source record ffba3523f0edd14be3460d039f22a6b98c02fd9e. This record is retained from earlier public citations. View default cited record →
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.
Passage ID: dinitz-garg-goemans-flow:entry:lean:v1
Source item: lean
Source record: dinitz-garg-goemans-flow:source:lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v3
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
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
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Resource revision: ffba3523f0edd14be3460d039f22a6b98c02fd9e
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
243048c83defcaecf809840f9fd1f89c81dc4b9c7c19eff1b3725071a91c580fComplete formal proof reported externally
The endpoint 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 formalized boundary.
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 ↗