{"id":"palomar/PALOMAR-2026-09-03-000001","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/6099fe8d978db59f541f676f6b697c6f6ad594c0","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-03-000001-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05C38","msc:05C45","graph-theory","hamiltonian-cycles","lean-formalization"],"score":0,"title":"Ore's and Dirac's Theorems on Hamiltonian Cycles","trust":"high","domain":"math.CO","source":"palomar","authors":["Noah Cohen"],"reviews":0,"subject":"math.CO","summary":"A complete machine-checked Lean 4 formalization of Ore's theorem (1960) and Dirac's theorem (1952) on the existence of Hamiltonian cycles in simple graphs. Proves Ore's degree-sum condition via maximal path cycle-closure and connectivity arguments, and derives Dirac's minimum-degree theorem as a corollary. To the maintainers' knowledge, the theorem was not found in an exact declaration name, docstring, and type signature search of the pinned Mathlib revision (Mathlib v4.34.0-rc1).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"Note on Hamilton circuits","identifier":"","relationship":"formalizes"},{"title":"Some theorems on abstract graphs","identifier":"","relationship":"adapts"}]}