{"id":"palomar/PALOMAR-2026-09-26-000003","url":"https://github.com/ShengtongZhang-alt/lovasz-opus/tree/ee0085ddec79996279c7b52044659032e5cf8431","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-26-000003-v1.json","repo":"https://github.com/ShengtongZhang-alt/lovasz-opus","tags":["math.CO","msc:05C45","msc:05C25","msc:05C48","msc:05C50","msc:05C70","msc:05C80","graph-theory","hamilton-cycles","cayley-graphs"],"score":0,"title":"Hamilton cycles in Cayley graphs of polylogarithmic degree","trust":"high","domain":"math.CO","source":"palomar","authors":["Shengtong Zhang"],"reviews":0,"subject":"math.CO","summary":"A complete Lean 4 / Mathlib formalization of the following theorem: there are absolute constants C, n0 > 0 such that every connected Cayley graph Cay(G, S) on n >= n0 vertices whose degree d = |S| is at least C (log n)^13 / log log n contains a Hamilton cycle (Lovasz.hamiltonian_of_polylog_degree). Here G is a finite group, S is a connection set (S = S^-1 and 1 not in S, so the graph is |S|-regular), log is the natural logarithm, and connectivity is equivalent to S generating G. The theorem is a case of the Lovász conjecture (every connected vertex-transitive graph has a Hamilton path) in…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-26","reactions":{},"formalized":true,"formalizes":[{"title":"Hamilton cycles in Cayley graphs of polylogarithmic degree","identifier":"docs/Polylog_Cayley.pdf (this repository, at the submitted commit)","relationship":"formalizes"}]}