{"id":"palomar/PALOMAR-2026-10-28-000022","url":"https://github.com/jtraverso/three-flows/tree/2e0bc7c111b2e6d05d81ce9bd1c2dc58a4184f4c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000022-v1.json","repo":"https://github.com/jtraverso/three-flows","tags":["math.CO","msc:05C21","msc:05C40"],"score":0,"title":"Nowhere-zero 3-flows in 6-edge-connected graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the theorem of Lovász, Thomassen, Wu and Zhang: every finite 6-edge-connected simple graph has a nowhere-zero integer 3-flow (the weak 3-flow conjecture). The proof formalizes Theorem 3.1 of the paper (β-orientations of multigraphs modulo 3) and Tutte's lifting theorem. Only simple graphs are stated; the paper's multigraph version and its results on modulo k-orientations for k > 3 are not stated. Mathlib does not contain this theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"Nowhere-zero 3-flows and modulo k-orientations","identifier":"doi:10.1016/j.jctb.2013.06.003","relationship":"formalizes"}]}