{"id":"palomar/PALOMAR-2026-10-16-000016","url":"https://github.com/jtraverso/euler-petersen/tree/02c3f1a5327c5f066938860bb07e9fce226b36ca","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000016-v1.json","repo":"https://github.com/jtraverso/euler-petersen","tags":["math.CO","msc:05C45","msc:05C70","msc:05C20","graph-theory","eulerian-graphs","formal-verification","lean"],"score":0,"title":"Euler's theorem on Eulerian circuits and trails, and Petersen's 2-factor 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 the classical characterization of Eulerian graphs and of Petersen's 2-factor theorem, for finite simple graphs. (1) Euler–Hierholzer: a finite connected graph has an Eulerian circuit if and only if every vertex has even degree, and the circuit can start at any prescribed vertex. (2) Eulerian trails: a finite connected graph has an Eulerian trail if and only if it has 0 or 2 vertices of odd degree; when the odd vertices are exactly a and b, there is an Eulerian trail from a to b. (3) Eulerian orientations: if every degree is even, the edges can be oriented…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Solutio problematis ad geometriam situs pertinentis","identifier":"Euler Archive E53","relationship":"formalizes"},{"title":"Ueber die Möglichkeit, einen Linienzug ohne Wiederholung und ohne Unterbrechung zu umfahren","identifier":"doi:10.1007/BF01442866","relationship":"formalizes"},{"title":"Die Theorie der regulären graphs","identifier":"doi:10.1007/BF02392606","relationship":"formalizes"}]}