{"id":"palomar/PALOMAR-2026-10-15-000020","url":"https://github.com/jtraverso/menger-hamiltonian/tree/35c5f684f9bfbd244bd0999ce725623ab571adb6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-15-000020-v2.json","repo":"https://github.com/jtraverso/menger-hamiltonian","tags":["math.CO","msc:05C40","msc:05C45","msc:05C38","msc:05C35","graph-theory","hamiltonian-cycles","formal-verification","lean"],"score":0,"title":"Menger's theorem, Hamiltonian cycles, long cycles and pancyclicity","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Menger's theorem for finite graphs (set form with a minimum separator and as many vertex-disjoint paths, two-vertex form, edge form for Mathlib's IsEdgeReachable, and the global edge form for Mathlib's IsEdgeConnected) and of classical sufficient conditions for Hamiltonian cycles: the Bondy–Chvátal closure step, Ore's and Dirac's theorems, and the Chvátal–Erdős theorem (k-connected with independence number at most k implies Hamiltonian), whose proof uses Menger's theorem through the fan lemma. Version 2 adds the Erdős–Gallai theorems on long paths and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"Zur allgemeinen Kurventheorie","identifier":"doi:10.4064/fm-10-1-96-115","relationship":"formalizes"},{"title":"Some theorems on abstract graphs","identifier":"doi:10.1112/plms/s3-2.1.69","relationship":"formalizes"},{"title":"Note on Hamilton circuits","identifier":"doi:10.2307/2308928","relationship":"formalizes"},{"title":"A method in graph theory","identifier":"doi:10.1016/0012-365X(76)90078-9","relationship":"formalizes"},{"title":"A note on Hamiltonian circuits","identifier":"doi:10.1016/0012-365X(72)90079-9","relationship":"formalizes"}]}