launch-corpus · graph-theory · open-problem · nowhere-zero-flows · bridgeless-graphs
Let G be a finite bridgeless graph. Does G admit a nowhere-zero 5-flow, i.e. an orientation of its edges together with an integer value f(e) on each edge with 0 < |f(e)| < 5 such that at every vertex the sum of the values on incoming edges equals the sum on outgoing edges?
Why it matters
Open Problem Garden rates the problem "Outstanding": for planar graphs it follows from flow/colouring duality and the five-colour theorem, so it is a sweeping generalization of that theorem; the Petersen graph has no nowhere-zero 4-flow, so 5 would be best possible. Seymour's 6-flow theorem (1981) is the best general result recorded there.
Mathematical status
Open: Open Problem Garden lists it as an open conjecture of Tutte, and Wikipedia's nowhere-zero flow article lists the 5-flow conjecture as unsolved as of 2026 (checked 2026-09-11).
Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.
Sources and provenance
Open Problem Garden entry: statement, attribution to Tutte (1954), partial results of Jaeger, Kilpatrick and Seymour, and open status (checked 2026-09-11): https://www.openproblemgarden.org/op/5_flow_conjecture
Definition of k-flows as integer circulations with 0 < |φ(e)| < k, and the list of Tutte's 3-, 4- and 5-flow conjectures as unsolved (checked 2026-09-11): https://en.wikipedia.org/wiki/Nowhere-zero_flow
Local target: Corpus.TutteFiveFlow.conjecture
Source SHA-256: db291859ebe85b1ba4bfb1add3535f84702d8e8a47954de74c75dae4dba68088
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
Every finite bridgeless simple graph (Mathlib SimpleGraph, no edge an IsBridge) admits an antisymmetric function f : V → V → ℤ that is nonzero exactly on adjacent pairs, has |f u v| < 5, and satisfies Kirchhoff's law ∑ u, f v u = 0 at every vertex; orientation is implicit in the
No public records on this page.
No public records on this page.