{"id":"palomar/PALOMAR-2026-10-18-000022","url":"https://github.com/jtraverso/robbins-strong-orientation/tree/076e734e9949720d3e4fcc2cc3cad4284871442c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000022-v1.json","repo":"https://github.com/jtraverso/robbins-strong-orientation","tags":["math.CO","msc:05C20","msc:05C40","graph-theory","orientations","lean"],"score":0,"title":"Robbins' theorem on strongly connected orientations","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Robbins' theorem: a finite connected simple graph has a strongly connected orientation (a digraph with underlying graph G, never containing both u → v and v → u, in which every vertex reaches every other) if and only if no edge of it is a bridge. As a corollary, every finite 2-edge-connected graph on a nonempty vertex type has a strongly connected orientation. Mathlib has bridges, edge connectivity and digraphs, but not this theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"A Theorem on Graphs, with an Application to a Problem of Traffic Control","identifier":"doi:10.2307/2303897","relationship":"formalizes"}]}