Hamilton cycles in Cayley graphs of polylogarithmic degree
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-26-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-26-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-26-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'