{"id":"palomar/PALOMAR-2026-10-16-000004","url":"https://github.com/jtraverso/petersen-matching/tree/77630d6771d3f5a3da2185db2ff451f6c6ed5190","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000004-v1.json","repo":"https://github.com/jtraverso/petersen-matching","tags":["math.CO","msc:05C70","graph-theory","perfect-matching","formal-verification","lean"],"score":0,"title":"Petersen's 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 Petersen's theorem: a finite 3-regular graph in which no edge is a bridge has a perfect matching; moreover, every edge of such a graph lies in some perfect matching. Both statements are derived from Tutte's theorem (in Mathlib) by counting the edges that leave the odd components.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"Die Theorie der regulären graphs","identifier":"doi:10.1007/BF02392606","relationship":"formalizes"}]}