Formal target: Corpus.TutteFiveFlow.conjecture

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 sign, and the simple-graph restriction is equivalent to the multigraph statement via edge subdivision.

Exact formal statement

∀ {V : Type} [inst : Fintype.{0} V] (G : SimpleGraph.{0} V),
  Corpus.TutteFiveFlow.Bridgeless G → Exists.{1} fun f => Corpus.TutteFiveFlow.IsNowhereZeroFlow G 5 f

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record