{"id":"palomar/PALOMAR-2026-11-01-000032","url":"https://github.com/jtraverso/komlos-szemeredi-hamiltonicity/tree/9a69e6d92eb29200d50580b9a54d07a4b37c28b8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000032-v1.json","repo":"https://github.com/jtraverso/komlos-szemeredi-hamiltonicity","tags":["math.CO","math.PR","msc:05C80","msc:05C45"],"score":0,"title":"The Hamiltonicity threshold of the random graph G(n, p) (Komlós–Szemerédi)","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 sharp Hamiltonicity threshold of the binomial random graph: if ω(n) → ∞, then G(n, (log n + log log n + ω(n))/n) is Hamiltonian with probability tending to 1, and G(n, (log n + log log n − ω(n))/n) is Hamiltonian with probability tending to 0 (Komlós–Szemerédi 1983; Bollobás 1984). The edge probability is clipped to [0, 1] (min 1 above, max 0 below). The statements are given in the finite product model of the registered entry PALOMAR-2026-10-28-000021 (one independent Bernoulli(p) coin per pair of distinct vertices of Fin n) and, as corollaries, for…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Limit distribution for the existence of Hamiltonian cycles in a random graph","identifier":"doi:10.1016/0012-365X(83)90021-3","relationship":"formalizes"},{"title":"Long paths and Hamiltonicity in random graphs","identifier":"arXiv:1507.00205","relationship":"adapts"}]}