{"id":"palomar/PALOMAR-2026-10-03-000003","url":"https://github.com/WozMit/hitting-time-loose-hamilton/tree/594001afb0fb7d80c581d0e2998a98355e87143c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-03-000003-v1.json","repo":"https://github.com/WozMit/hitting-time-loose-hamilton","tags":["math.CO","msc:05C65","msc:05C80","random-graphs","combinatorics","hamilton-cycles","lean-formalization"],"score":0,"title":"The hitting time for loose Hamilton cycles in r-graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Jared León"],"reviews":0,"subject":"math.CO","summary":"A Lean formalisation of a hitting time theorem of Wanfang Chen, Jared León and Xizhi Liu. For every fixed integer r ≥ 3, assume all r-element subsets of n vertices are exposed in a uniformly random order. As n tends to infinity through multiples of r − 1, with probability tending to one, a loose Hamilton cycle first emerges exactly when the last isolated vertex disappears.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-03","reactions":{},"formalized":true}