{"id":"palomar/PALOMAR-2026-10-28-000004","url":"https://github.com/jtraverso/nash-williams-orientation/tree/3412d885cf3ba6680770cb8014df96af8fa3d042","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000004-v1.json","repo":"https://github.com/jtraverso/nash-williams-orientation","tags":["math.CO","msc:05C20","msc:05C40"],"score":0,"title":"Nash-Williams' weak orientation 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 Nash-Williams' weak orientation theorem (1960): every 2k-edge-connected finite graph has a k-arc-connected orientation, i.e. one in which every nonempty proper vertex set is left by at least k arcs. It is proved for finite loopless multigraphs given by an edge family, and stated for simple graphs with Mathlib's SimpleGraph.IsEdgeConnected and orientations as Mathlib Digraphs. The proof is by induction on the number of edges, with Mader's lemma (a minimally 2k-edge-connected multigraph has a vertex of degree 2k) and Lovász's splitting lemma, both proved in…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"On Orientations, Connectivity and Odd-Vertex-Pairings in Finite Graphs","identifier":"doi:10.4153/CJM-1960-049-6","relationship":"formalizes"}]}