Hamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjecture
Every connected Cayley graph on n vertices with degree at least C(log n)^13/log log n has a Hamilton cycle, lowering the degree threshold in the Cayley-graph form of the Lovász conjecture from a power of n to a power of log n; the manuscript was drafted by GPT 6 Pro and the proof formalized in Lean by Claude agents.
- Lab
- Independent
- Model
- GPT 6 Pro (manuscript draft); Claude Opus 5.5 agents in Grok Build (Lean formalization)
- Field
- Mathematics
- Date
- 2026-09-26
- Human collaborators
- Domagoj Bradač, Matija Bucić, Micha Christoph, Zach Hunter, Oliver Janzer, Alp Müyesser, Shengtong Zhang
- Problem posed
- 1969 · open 57 yrs
What was found
Lovász asked in 1969 whether every connected vertex-transitive graph has a Hamilton path; the Cayley-graph form asks whether every connected Cayley graph on at least three vertices is Hamiltonian. For arbitrary connected Cayley graphs this was known for linear degree (Christofides, Hladký and Máthé, 2014) and for degree at least n^(1-c) (Bedert, Draganić, Müyesser and Pavez-Signé, arXiv:2603.08675). The research draft dated 25 September 2026 lowers the threshold to C(log n)^13/log log n through local absorption, signed rounding, a weighted partition and a connecting system. The repository formalizes the whole draft as a DAG of about 55 lemmas in roughly 36,500 lines, including classical inputs the paper uses without proof, and states the theorem in a Mathlib-only Challenge.lean using Mathlib's own Cayley graph and Hamiltonicity definitions.
Novelty check
The README's context section and a web search place the result in an active 2026 line of work: the n^(1-c) threshold of arXiv:2603.08675, Hamiltonicity of regular sublinear expanders (arXiv:2605.15043), a sublinear-expander approach to the Lovász conjecture (arXiv:2606.09742) and almost Hamilton cycles at polylogarithmic degree (arXiv:2609.30165). Each of those papers has at least one of the draft's named authors, so the draft reads as the continuation of that program rather than a result competing with it; the 2026-09-28 watch run's concern that it might be superseded by that literature confused the two. No earlier result giving full Hamiltonicity at polylogarithmic degree was found. The draft builds on three unpublished manuscripts listed in its bibliography, which are not public, so what is new in the draft relative to them cannot be checked.
Caveats and known objections
The draft calls its own proof a consolidated proposed proof, not an independently verified theorem, and the PDF carries no author line: the six authors are named by the repository's maintainer, Shengtong Zhang, who directed the formalization, wrote no Lean and is not an author of the manuscript. No human has reviewed the Lean statement or proof; the statement was audited by the formalizing agent and by agent runs of Palomar's review policy. Graded claimed for that reason, since a Palomar registration shows the proof typechecks against the recorded statement, not that the statement is the theorem. Autonomy is collaborative on the disclosure's own wording, that GPT 6 Pro prepared the draft with significant input from the authors including unpublished human manuscripts; how much of the argument is the model's and how much the manuscripts' is not documented, and if it proves to be mostly the latter the grade should move down to ai-assisted. The formalization is entirely agent-written, by 38 parallel subagents under a coordinating agent. Unrefereed, and days old at entry.
Machine-checked elsewhere
PalomarPALOMAR-2026-09-26-000003
ShengtongZhang-alt/lovasz-opus at ee0085ddec79 · checked 2026-09-26
ProvedLovasz.hamiltonian_of_polylog_degree
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Hamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjecture. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-26-lovasz-cayley-polylog-degreeBibTeX
@misc{whataifound-independent-2026-degree,
title = {Hamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjecture},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Claimed. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-09-26-lovasz-cayley-polylog-degree}
}