Papers With

← All papers
First page of Hitting time for loose Hamilton cycles in the random hypergraph process

Hitting time for loose Hamilton cycles in the random hypergraph process

Jared León, Xizhi Liu

math.CO Oct 21, 2026 · v1
formalization combinatorics probability ai-agents
Read PDF arXiv abstract Code
TL;DR
Provides a Lean 4 formalisation, produced largely by an LLM, of the hitting-time theorem for loose Hamilton cycles in r-uniform hypergraphs with (r-1)|n.
Abstract
The random hypergraph process starts with an empty hypergraph on $n$ vertices and adds a uniformly chosen missing edge at each step. For even $n$, we prove that, with high probability, a $3$-uniform loose Hamilton cycle appears when the last isolated vertex disappears. The approach developed here adapts arguments from Kahn's work on perfect matchings. It can also be extended to obtain the corresponding hitting-time theorems for $r=2$ and every fixed $r\ge4$ satisfying $(r-1)\mid n$. Furthermore, it can be used to estimate the numbers of loose Hamilton cycles at these hitting times for every fixed $r\ge2$, up to a factor of $\exp\{o(n)\}$.
Problem

In the random 3-uniform hypergraph process on n vertices (n even), the question is whether a loose Hamilton cycle appears exactly when the last isolated vertex disappears. Kühn–Osthus and Frieze–Pérez-Giménez posed this as an open problem.

Approach

The proof adapts Kahn's entropy, conditioned-sampling and random edge-deletion arguments for perfect matchings. It reduces the problem to counting mixed Hamilton cycles in a conditioned core with prescribed degree lower bounds. Entropy stability then gives near-uniform edge marginals. The extension to general r was developed semi-automatically and formalised in Lean 4 by a large language model, with gaps found during formalisation repaired using GPT.

Results

With high probability, the hitting time of a 3-uniform loose Hamilton cycle equals the hitting time of minimum degree 1. Analogous results hold for r=2 and every fixed r≥4 with (r-1)|n, along with cycle-count estimates up to a factor exp{o(n)}. The Lean 4 formalisation, registered as a Palomar entry, covers every r≥3 with (r-1)|n.