{"id":"palomar/PALOMAR-2026-10-18-000009","url":"https://github.com/jtraverso/jaeger-four-flow/tree/623dd0dd718f93de06d4dc792e116dd32ef97553","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000009-v3.json","repo":"https://github.com/jtraverso/jaeger-four-flow","tags":["math.CO","msc:05C21","msc:05C40","nowhere-zero-flows","graph-theory","lean"],"score":0,"title":"Jaeger's 4-flow and 8-flow theorems and Seymour's 6-flow theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Jaeger's 4-flow theorem: every finite 4-edge-connected simple graph has a nowhere-zero integer 4-flow, i.e. an antisymmetric function on darts with values in {±1, ±2, ±3} that is conserved at every vertex. Also proved: a graph with two edge-disjoint spanning trees has its edges covered by two even subgraphs (a nowhere-zero ℤ₂ × ℤ₂-flow) and has a nowhere-zero integer 4-flow. Version 2 adds Jaeger's 8-flow theorem: every finite bridgeless graph has its edges covered by three even subgraphs and has a nowhere-zero integer 8-flow; conversely a graph with a…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"Flows and generalized coloring theorems in graphs","identifier":"doi:10.1016/0095-8956(79)90057-1","relationship":"formalizes"},{"title":"Nowhere-zero 6-flows","identifier":"doi:10.1016/0095-8956(81)90058-7","relationship":"formalizes"},{"title":"A contribution to the theory of chromatic polynomials","identifier":"doi:10.4153/CJM-1954-010-9","relationship":"formalizes"}]}