The Lovász conjecture — four exceptions; the search space for a fifth splits three ways by the deficiency def
Only four connected vertex-transitive graphs without a Hamiltonian cycle are known, apart from K₂. All four have a path but no cycle — which is why the path conjecture has not fallen. This article constructs and checks those four, sweeps 9,805 Cayley graphs, builds Hamilton cycles on the floor directly above Petersen and Coxeter, and then asks where a fifth exception could be, splitting the search space into three boxes by the deficiency def = |V| − length of a longest cycle.
Leanmachine-checked (Lean 4 + mathlib, standard axioms only, no sorryAx, no native_decide; theorem names given)
paperproved, not yet machine-checked
computationchecked on this machine, within the range stated; not a claim made to the outside
knowna restatement, a known theorem, or a check of the literature
- What the problem is
- How far the world has come — four exceptions; cubic graphs exhaustively checked to 1,280 vertices
- What was done ①: constructing the four exceptions and checking them
- What was done ②: sweeping 9,805 Cayley graphs
- What was done ③: two cycles on the floor above Petersen and Coxeter
- Where is the fifth one? — three boxes by the deficiency def
- What remains
- Sources and reproduction
What the problem is
A question from 1970.
Does every connected vertex-transitive graph have a Hamiltonian path?
(Vertex-transitive = every vertex looks the same by symmetry. Hamiltonian path = a walk through every vertex exactly once.)
It is still open. And the reason this conjecture has survived 56 years lies inside just four graphs.
How far the world has come
| Question | State |
|---|---|
| Does every connected vertex-transitive graph have a Hamiltonian path | open (since 1970) |
| Does every connected vertex-transitive graph have a Hamiltonian cycle | False. Four exceptions are known (five counting K₂) |
| Does every Cayley graph have a Hamiltonian cycle (|G| > 2) | Open. Not a single counterexample has been found |
| The known exceptions | Petersen / Coxeter / the truncation of each (and K₂) |
| Cubic vertex-transitive graphs | All 111,360 of them up to 1,280 vertices have been checked exhaustively; the exceptions are exactly the four known ones (Potočnik–Spiga–Verret)known |
| The census of vertex-transitive graphs in general | up to 47 vertices (arXiv:1811.09015)known |
| Groups of order p², p³, p⁴, 2p² | no exceptions (Du–Kutnar–Marušič). The general case 2pq is open |
| The dense case | settled (Christofides–Hladký–Máthé). ⟹ a fifth exception would be sparse |
What is distinctive about this problem is how few the exceptions are. And all four have no cycle but do have a path — which is why the path conjecture has not fallen. If there is a fifth, then at least among cubic graphs it lies above 1,280 vertices, and it is sparse.
What was done ① — constructing the four exceptions and checking them
Of the connected vertex-transitive graphs with no Hamiltonian cycle (returning to the start), the four other than K₂ (a single edge) were constructed and checked by machine. computation
| Graph | Vertices | Edges | Degree | Girth | |Aut| | Vertex-transitive | Hamiltonian cycle | Hamiltonian path | def |
|---|---|---|---|---|---|---|---|---|---|
| Petersen | 10 | 15 | 3 | 5 | 120 | True | False | True | 1 |
| Coxeter | 28 | 42 | 3 | 7 | 336 | True | False | True | 1 |
| Truncated Petersen | 30 | 45 | 3 | 3 | 120 | True | False | True | 3 |
| Truncated Coxeter | 84 | 126 | 3 | 3 | 336 | True | False | True | 3 |
The last column, def, is the deficiency |V| − length of a longest cycle (§06). The longest cycle of the Coxeter graph has length 27; a hypohamiltonian graph is forced to have circumference |V| − 1.
All four have no cycle, but do have a path.
That is the substance of why the conjecture is still alive. Had it been the cycle conjecture, counterexamples would have settled it long ago. The path conjecture has not fallen.
The |Aut| column shows that the four are really two. Truncation leaves the automorphism group unchanged (120 and 336 appear twice), and the vertex counts merely triple: 30 = 3×10, 84 = 3×28. ⟹ The known exceptions are "two primitive ones + their two truncations", which is essentially two. And truncation stops after one step (§06).
Look at the smallest example, the Petersen graph.
The path is 0 → 1 → 2 → 3 → 4 → 9 → 6 → 8 → 5 → 7, visiting all 10 vertices once each. But there is no edge back from 7 to 0. The same holds for every other path, and one can confirm that it cannot be closed.
What was done ② — sweeping 9,805 Cayley graphs
The conjecture has a stronger form.
Cayley version (open): every connected Cayley graph of a finite group with |G| > 2 has a Hamiltonian cycle.
This one is about cycles. A single counterexample would be a major event. Up to generating sets of size 2, as many as could be built were built, and all of them checked. computation
| Family | Groups | Cayley graphs | Without a Hamiltonian cycle |
|---|---|---|---|
| Cyclic Z₃–Z₃₀ | 28 | 3,748 | 0 |
| Dihedral D₃–D₁₅ | 13 | 1,320 | 0 |
| Symmetric S₃, S₄, S₅ | 3 | 3,537 | 0 |
| Alternating A₄, A₅ | 2 | 1,188 | 0 |
| Quaternion Q₈ | 1 | 12 | 0 |
| Total | 47 | 9,805 | 0 |
The heaviest was S₅ (order 120, 3,420 graphs, 559 s), then A₅ (order 60, 1,140 graphs, 138 s).
Every group is used only after its constructed order has been compared with the expected one. A wrong choice of generators can produce a group named A₅ whose contents are A₄ (order 12) — two 3-cycles fixing the same point generate the stabiliser of that point. So before the sweep begins, assert len(G) == expected order is passed for every group. An is generated by a 3-cycle and an n-cycle when n is odd.
The choice of tool changes the order of magnitude
Vertex-transitivity is decided not by enumerating all isomorphisms but by backtracking pruned by the distance partition; Hamiltonicity not by reassembling "position variables + allowed pairs" but by the solver's own circuit constraint (AddCircuit in CP-SAT). What would not finish in 570 seconds took 2.3 seconds. "There is a Hamiltonian cycle" is a constraint the solver already has.
What test this sweep actually is. Sweeping 9,805 Cayley graphs is a test of the stronger Cayley version. The four known exceptions are not Cayley graphs, so no amount of sweeping Cayley graphs will produce the fifth one. How to look for a fifth is the subject of §06.
What was done ③ — two cycles on the floor above Petersen and Coxeter
The Petersen graph (10 vertices) and the Coxeter graph (28 vertices) are in fact the first floors of families of graphs built from matrices. Take invertible Hermitian matrices over F₄ as vertices and join them when the rank of the difference is 1, and you get a family HGLn(F₄) whose n = 2 is Petersen. Do the same with invertible symmetric matrices over F₂ and you get SGLn(F₂), whose n = 3 is Coxeter. Orel (2015) posed "does the upper floor of this family have a Hamiltonian cycle?" as an open problem, and found cycles in the three cases on 280, 448 and 13,888 vertices with the Concorde TSP solver, leaving the general case open.
Cycles were constructed on that next floor, for two of them. computation
| Graph | Vertices | Vertex-transitive | Hamiltonian cycle |
|---|---|---|---|
| HGL₂(F₄) = Petersen | 10 | ○ | none (classical) |
| SGL₃(F₂) = Coxeter | 28 | ○ | none (classical) |
| HGL₃(F₄) / SGL₄(F₂) / SGL₅(F₂) | 280 / 448 / 13,888 | ○ / × / ○ | yes (Orel 2015) |
| HGL₄(F₄) | 38,080 | ○ | yes (this machine) |
| SGL₆(F₂) | 888,832 | × | yes (this machine) |
| HGL₅(F₄) / SGL₇(F₂) | 18,887,680 / 112,881,664 | ○ | undecided |
The method is Pósa rotation and extension — when the end of a path can no longer be extended, reverse the path at a neighbour of the end; an old heuristic. Encoding vertices as bit strings of the matrix makes adjacency a matter of XOR alone, so it runs without holding an adjacency list. 38,080 vertices took 0.8 seconds; 888,832 vertices about 17 minutes. The cycles themselves, and verifiers that run on the standard library alone, are distributed here (checking takes 1.4 s and 35.5 s, and the verdict was reproduced by an independent implementation).
What cannot be said. A heuristic can only say "there is one". Whether there is "none" is not settled here for any graph. No construction for general n is given either. Each family has simply gained one point on the affirmative side. Nor is any claim made that this is not already known: within the range searched — general searches on five queries, and all six papers citing Orel 2015 — no reference stating the Hamiltonicity of these two was found, but MathSciNet, zbMATH, conference proceedings tables of contents and non-English literature were not consulted.
Relation to the question of this article. A fifth exception would be a graph that is connected, vertex-transitive and has no Hamiltonian cycle. HGL₄(F₄) is vertex-transitive and was therefore a candidate, but a cycle was found, so it is out. SGL₆(F₂) is not vertex-transitive and was never a candidate. So these two did not find a fifth exception; they confirmed that there is no fifth exception on the floor directly above Petersen and Coxeter.
Where is the fifth one? — three boxes by the deficiency def
"Is there a Hamiltonian cycle" is a coarse 0/1 quantity. Measured by the length of a longest cycle instead, it becomes a number.
This quantity has a name, the perimeter gap (Alspach 1981), and for vertex-transitive graphs def = 1 ⟺ hypohamiltonian (the one vertex missed by a cycle of length |V| − 1 can be moved to any vertex by vertex-transitivity). The four known exceptions have def 1, 1, 3, 3. The search space splits three ways by this number.
| Box | Condition | Known inhabitants | State |
|---|---|---|---|
| I | def = 1 (hypohamiltonian) | Petersen, Coxeter | cubic graphs exhaustively checked to 1,280 verticesknown |
| II | truncations; def ≡ 0 (mod 3) | the two truncations (def = 3) | empty up to 3,840 vertices — a truncation T(H) has 3|V(H)| vertices, and T(H) is Hamiltonian whenever H is (lemma: circ(T(H)) = 3·circ(H))paper |
| III | def ≥ 2 and not a truncation | none | no vertex-transitive example is known at all |
The truncation operator freezes after one generation. T(G) is vertex-transitive exactly when G is arc-transitive, and T(G) itself is not edge-transitive, so T²(G) is never vertex-transitive. Moreover T(G) is Hamiltonian ⟺ G is Hamiltonian. paper So the inhabitants of box II are exactly the truncations of "cubic arc-transitive graphs other than Petersen and Coxeter with no Hamiltonian cycle", and that census (the Foster census) is published. What is left is box III.
At the front of box III — the def = 2 conjecture
Conjecture (B135′). No connected vertex-transitive graph has def = 2.
This statement is smaller than a fifth exception, but not easier. Grünbaum conjectured in 1974 that for k ≥ 2 there is no graph with circ = n − k in which every induced subgraph of order n − k is Hamiltonian, and B135′ contains the vertex-transitive case of that conjecture. known Further, in a regular bipartite graph every cycle is even, so def is even — def = 1 is impossible for bipartite graphs, and truncations contain triangles, so they are not bipartite. ⟹ A non-Hamiltonian bipartite vertex-transitive graph, if there is one, necessarily lies in box III, and the smallest such case is the front of B135′. paper
Drop vertex-transitivity, and def = 2 does occur
The cubic bipartite graphs known as counterexamples to Tutte's conjecture — Ellingham–Horton 54 and 78, Horton 96 — all have def = 2 (circumference 52, 76, 94). computation How small can a cubic bipartite graph with def = 2 be?
LeanShiori1161.G30_def2, Shiori1193.G30b_def2, Shiori1193.G30c_def2 — all three state the same thing: (∀ v, G.degree v = 3) ∧ G.Colorable 2 ∧ G.Connected ∧ (∃ c : G.Walk 0 0, c.IsCycle ∧ c.length = 28) ∧ (∀ v (c : G.Walk v v), c.IsCycle → c.length ≤ 28) ∧ ¬ G.IsHamiltonian. Non-Hamiltonicity is closed by running the search inside the kernel (no external certificate). That none exists on 28 or fewer vertices, and that there are exactly three classes on 30, is an exhaustive enumeration on this machine — with no assumptions (3-connectivity, symmetry and girth are not imposed), agreeing along two independent routes. computation The graphs are 24 vertices smaller than Ellingham–Horton 54 and, unlike the known examples, not 3-connected.
With the same machinery, if def = 2 is not required, there is a non-Hamiltonian cubic bipartite graph on 20 vertices (circumference 14). LeanShiori1193.G20_def6 That none exists on 18 or fewer vertices, and uniqueness, are computation. computation
Raising the degree empties things out. No 4-regular bipartite graph with def = 2 exists on n ≤ 24 vertices — exhaustive, no symmetry assumed. computation This is the smallest range of Häggkvist's 1976 conjecture (a 2-connected k-regular bipartite graph on n ≤ 6k vertices is Hamiltonian) for k = 4, and there the "def = 2 counterexample" is gone. Impose one step of symmetry and paper gives lower bounds: a semisymmetric graph (regular, edge-transitive, not vertex-transitive) with def = 2 has n ≥ 50 if cubic and n ≥ 26 if 4-regular. paper The engine is "connected, d-regular and edge-transitive ⟹ edge-connectivity d", which closes the decomposition along 2-edge cuts under edge-transitivity.
A counting theorem — Hamilton cycles of GP(n,3)
For the generalised Petersen graph GP(n,3) (outer n-cycle, inner rim of step 3, n spokes):
Theorem. If n is odd and n ≥ 7, the number of Hamilton cycles of GP(n,3), counted as edge sets, is divisible by n.
LeanShiori1202.gp3_dvd_hc_odd (standard axioms only, no sorry). For n = 7, 9, 11, 13, 15 the counts are 7, 9, 11, 26, 75, also in Lean (Shiori1168.GP7_hc_card … GP15_hc_card). The skeleton of the proof: the rotation ρ acts freely — a Hamilton cycle invariant under ρj would descend to a 2-factor of winding number 0 on the quotient, which a window count and the sign of a permutation rule out — so n ∣ #HC by Burnside. This quantity is invariant under automorphisms, so it cannot be used to prove non-Hamiltonicity. Within the range searched it was not found in print (OEIS has no sequence of the counts; arXiv:2503.08326 gives the values by a linear recurrence, not the classification).
The smallest order of a cubic bipartite graph with def = 2, and the GP(n,3) theorem, are each being written up separately as a short paper. in preparation
What remains
Where the open items that have moved now stand is collected in What remains. Only what is open at present is listed here.
| Content | |
|---|---|
| could say | Among 47 groups and 9,805 Cayley graphs, none lacks a Hamiltonian cyclecomputation |
| could say | The four known exceptions all have no cycle but do have a path. They are essentially two, and truncation freezes after one generationpaper |
| could say | HGL₄(F₄) and SGL₆(F₂) have Hamiltonian cyclescomputation (certificates distributed) |
| could say | A cubic bipartite graph with def = 2 exists on 30 verticesLean and none on 28 or fewercomputation / n ∣ #HC(GP(n,3)) for odd n ≥ 7Lean |
| cannot say | The conjecture itself. A sweep looks for counterexamples; it is not a proof that none exist |
| cannot say | Generating sets of size 3 or more (only up to 2 was examined); groups of order 130 and above (A₆ was skipped). Both are tests of the Cayley version, not the search for a fifth exception |
Open at present
| Open item | Where it stops |
|---|---|
| B135′ (no connected vertex-transitive graph has def = 2) | On paper: a cubic one is forced to have girth ≥ 4, and the three mechanisms behind counterexamples (an excess of independent sets; a 3-edge cut with cycles on both sides; partial truncation) are each killed by vertex-transitivity through a separate theorem. Impossibility is not established. The 4-regular bipartite case n = 26 has not been run |
| Whether box III is empty | Whether a vertex-transitive graph with def ≥ 2 that is not a truncation exists at all. Restricted to cubic graphs, it can only lie above 1,280 vertices |
| Machine-checking the minimality | Putting "no cubic bipartite graph with def = 2 on 28 or fewer vertices" through the kernel is decided by memory (an estimated 150 GiB at the current node count). The structure of the enumeration has to change |
Sources and reproduction
| Item | Kind | Source / tool |
|---|---|---|
| The Lovász conjecture (1970) | conjecture | does every vertex-transitive graph have a Hamiltonian path |
| Four exceptions without a Hamiltonian cycle (and K₂) | known | Petersen / Coxeter / the truncation of each |
| Construction and verification of the four exceptions | computed on this machine | Coxeter identified by fingerprint (28 vertices, 3-regular, girth 7, vertex-transitive, non-Hamiltonian) |
| The Hamiltonian path in Petersen | computed on this machine | 0→1→2→3→4→9→6→8→5→7 |
| The sweep of 9,805 Cayley graphs | computed on this machine | CP-SAT AddCircuit. 841 s. Every group passes an order assertion before the sweep begins |
| Exhaustive check of 111,360 cubic vertex-transitive graphs (to 1,280 vertices) | literature | Potočnik–Spiga–Verret, arXiv:1201.5317 |
| Complete census of vertex-transitive graphs (to 47 vertices) | literature | arXiv:1811.09015 |
| Classification by order family (no exceptions for p², p³, p⁴, 2p²) | theorem | Du–Kutnar–Marušič, Combinatorica 41 |
| Settlement of the dense case | theorem | Christofides–Hladký–Máthé, arXiv:1008.2193 |
| The three truncation theorems and the Foster census | known | T(G) has a Hamiltonian cycle ⟺ G does / Aut(T(G)) ≅ Aut(G) / T(G) vertex-transitive ⟺ G arc-transitive |
| Orel's families (HGLₙ(F₄), SGLₙ(F₂)) and open problem 16 | literature | Orel, Electron. J. Combin. 22 (2015) |
| Hamiltonian cycles in HGL₄(F₄) and SGL₆(F₂) | computed on this machine | Pósa rotation + extension. Cycles and standard-library-only verifiers distributed (reproduced by an independent implementation) |
| The name and the question of the perimeter gap | literature | Alspach 1981 |
| Grünbaum's conjecture (the uniform classes with circ = n − k are empty for k ≥ 2) | literature | Grünbaum 1974 (via the abstract of arXiv:2602.19669) |
| circ(T(H)) = 3·circ(H); truncation freezes | paper | elementary; very possibly in print already |
| def = 2 for Ellingham–Horton 54, 78 and Horton 96 | computed on this machine | longest cycles by SAT. Circumference 52, 76, 94 |
| Cubic bipartite graphs with def = 2: three classes on 30 vertices | machine-checked | Shiori1161.G30_def2, Shiori1193.G30b_def2, G30c_def2. Axioms in the ledger of the Lean verification bundle |
| None on 28 or fewer vertices; exactly three classes on 30 | computed on this machine | exhaustive enumeration of chord diagrams (no assumptions) and decomposition along 2-edge cuts, two routes. The 3-connected minimum 50 is Brinkmann–Zamfirescu, arXiv:2101.00943 |
| A non-Hamiltonian cubic bipartite graph on 20 vertices | machine-checked / computation | Shiori1193.G20_def6. Minimality and uniqueness computed on this machine |
| No 4-regular bipartite graph with def = 2 on n ≤ 24 | computed on this machine | exhaustive. Häggkvist's 1976 conjecture via Jackson–Li, JCTB 62 (1994) |
| Semisymmetric with def = 2 ⟹ n ≥ 50 (cubic), n ≥ 26 (4-regular) | paper | edge-transitive ⟹ edge-connectivity = degree. The cubic case is subsumed by arXiv:2602.14388 (cubic semisymmetric graphs on fewer than 3,000 vertices are Hamiltonian) |
| n odd ⟹ n ∣ #HC(GP(n,3)); the counts for n = 7–15 | machine-checked | Shiori1202.gp3_dvd_hc_odd, Shiori1168.GP{7,9,11,13,15}_hc_card. Axioms in the ledger of the Lean verification bundle |
Apart from the cycles of §05 and the two theorems of §06, there is no new mathematics in this article. The four exceptions, the Cayley version of the conjecture, and the ingredients of the three boxes (the truncation theorems, Grünbaum's conjecture, parity in bipartite graphs) are all known. Novelty is claimed only as far as "not found in the literature searched".
The reason the conjecture is alive lies directly inside the four exceptions. Every one of them has no cycle but does have a path. Surviving by a hair's breadth is the same shape that appears as "criticality" in the Riemann hypothesis and the Collatz conjecture.