{"id":"palomar/PALOMAR-2026-10-28-000021","url":"https://github.com/jtraverso/random-graph-thresholds/tree/86325faff71fb76c0769963525b69095fa0a6241","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000021-v1.json","repo":"https://github.com/jtraverso/random-graph-thresholds","tags":["math.CO","math.PR","msc:05C80","msc:05C45","msc:05C40"],"score":0,"title":"Hamiltonicity and connectivity thresholds of the random graph G(n, p)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of two classical threshold results for the binomial random graph G(n, p), modelled as a finite product probability space with one independent Bernoulli(p) coin per pair of vertices: Pósa's theorem (1976) that G(n, p) with p ≥ C log n / n is Hamiltonian with probability tending to 1, also stated with the explicit constant C = 80 (posa_eighty), and both sides of the Erdős–Rényi connectivity threshold (1959): G(n, (log n ± ω(n))/n) with ω(n) → ∞, the edge probability clipped to [0, 1], is connected with probability tending to 1, resp. 0. Hamiltonicity and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"Hamiltonian circuits in random graphs","identifier":"doi:10.1016/0012-365X(76)90068-6","relationship":"formalizes"},{"title":"On random graphs I","identifier":"doi:10.5486/PMD.1959.6.3-4.12","relationship":"formalizes"}]}