# P2584: Exact Hamiltonicity probability on eight labeled vertices

- ID: `P2584`
- Reference: `hamiltonian-graph-probability-eight`
- Page: https://theoremdb.org/statements/P2584
- Record maturity: Reviewed problem with recorded work

## Problem

Among all \(2^{28}\) simple graphs on eight labeled vertices, exactly how many contain a Hamilton cycle?

### Problem setup

- **Remark.** Each of the 28 possible edges is independently present or absent.
- **Definition.** A Hamilton cycle visits all eight vertices exactly once.

### What counts as a solution

- Return the exact numerator and a reproducible counting certificate, such as an upward-closure hash plus independent orbit check.

## The answer

The exact probability is 9,479,757 divided by 16,777,216, approximately 0.565037548542022705078125. [2](#reference-2)

**Review status:** Reproduced.

**Lean verification:** not Lean-verified.

### Verification

There are \(\binom82=28\) possible edges, so the uniform sample space contains \(2^{28}=268{,}435{,}456\) labeled simple graphs. Exactly
\[
151{,}676{,}112
\]
of them contain a Hamilton cycle. Thus
\[
\Pr(G\text{ is Hamiltonian})
=\frac{151{,}676{,}112}{268{,}435{,}456}
=\frac{9{,}479{,}757}{16{,}777{,}216}
=0.565037548542022705078125.
\]
The complementary count is \(116{,}759{,}344\). The Hamiltonian count exceeds half of the sample space by \(17{,}458{,}384\).

Two exhaustive computations reproduce the numerator. The first takes the upward closure of all 2,520 labeled Hamilton-cycle edge masks. The second generates all 12,346 isomorphism classes on eight vertices, finds 6,196 Hamiltonian classes, and sums the orbit weights \(8!/|\operatorname{Aut}(G)|\).

## Work

### Proof and evidence for the resolution

**Computation 1 (Exactly 151,676,112 labeled graphs on eight vertices are Hamiltonian).** The exact probability is 9,479,757 divided by 16,777,216, approximately 0.565037548542022705078125.

There are \(\binom82=28\) possible edges, so the uniform sample space contains \(2^{28}=268{,}435{,}456\) labeled simple graphs. Exactly
\[
151{,}676{,}112
\]
of them contain a Hamilton cycle. Thus
\[
\Pr(G\text{ is Hamiltonian})
=\frac{151{,}676{,}112}{268{,}435{,}456}
=\frac{9{,}479{,}757}{16{,}777{,}216}
=0.565037548542022705078125.
\]
The complementary count is \(116{,}759{,}344\). The Hamiltonian count exceeds half of the sample space by \(17{,}458{,}384\).

Two exhaustive computations reproduce the numerator. The first takes the upward closure of all 2,520 labeled Hamilton-cycle edge masks. The second generates all 12,346 isomorphism classes on eight vertices, finds 6,196 Hamiltonian classes, and sums the orbit weights \(8!/|\operatorname{Aut}(G)|\).

### Background and intake notes

The event first appears to exceed probability one half at eight vertices. An exact count would replace that simulation claim.

- Original intake status: Status unknown as a database target. The count may appear in an integer-sequence or graph-enumeration table.
- There are 2520 undirected Hamilton cycles on eight labeled vertices. Mark their 8-edge masks and take the upward closure by a Boolean zeta transform.
- A raw Boolean array has 2^28 entries. Chunked transforms or inclusion-exclusion over cycle orbits reduce memory pressure.

- Recorded example: Exact Hamiltonian graph counts for 3,4,5,6,7 vertices are 1,10,218,10078,896756.

### Prior approaches

- **Route 1** (supported): A326208 gives 151,676,112, A326207 gives 116,759,344, and the classical unlabeled sequence gives 6,196 classes. [2](#reference-2)

### Runnable artifacts

- **Artifact 1** (reproduced): A standard-library Python program marks every Hamilton cycle, closes upward under edge addition, and hashes the full truth table. [2](#reference-2)
- **Artifact 2** (reproduced): An isomorph-free generator and automorphism-group calculation give the same labeled total and edge histogram. [1](#reference-1)

### Computational notes

- Boolean zeta transforms over edge masks verified the exact counts through seven vertices. A seeded simulation of 200000 uniform eight-vertex graphs found 112912 Hamiltonian graphs, an estimated probability 0.56456. This last figure is simulation evidence only.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `hamiltonian-graph-probability-eight`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

An informal proof is recorded. A Lean formalization still needs to be attached.

[Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20hamiltonian-graph-probability-eight%0A%0AExact%20title%3A%20Exact%20Hamiltonicity%20probability%20on%20eight%20labeled%20vertices%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fhamiltonian-graph-probability-eight%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>Falk Hüffner, tinygraph: Exploring Graph Conjectures on Small Graphs, GitHub repository, commit 97665350689943d64b90ca1501b3291db0538a0a, May 8, 2019. pinned commit 9766535, graph-enumeration and Hamiltonicity routines invoked by the independent C++11 driver https://github.com/falk-hueffner/tinygraph/tree/97665350689943d64b90ca1501b3291db0538a0a
   - Also cited at Independent C++11 driver executed against tinygraph 9766535 and nauty 2.6r6 on 2026-07-24
   - software; primary source; commit 97665350689943d64b90ca1501b3291db0538a0a; checked 2026-08-01
   - Source use: code_used
   - Reused material: pinned commit 9766535, graph-enumeration and Hamiltonicity routines invoked by the independent C++11 driver
   - Reuse basis: fair_use_reviewed; rights holder: Falk Hüffner; checked 2026-08-01; by Philip Weiss, TheoremDB staff
   - Required attribution: Falk Hüffner, tinygraph: Exploring Graph Conjectures on Small Graphs, GitHub repository, commit 97665350689943d64b90ca1501b3291db0538a0a, May 8, 2019.
   - For Exact Hamiltonicity probability on eight labeled vertices, this source supplies the pinned implementation used to enumerate and test the eight-vertex graphs; the packet's driver supplies the exact count.
2. <a id="reference-2"></a>Gus Wiseman, “A326208: Number of Hamiltonian labeled simple graphs with n vertices,” The On-Line Encyclopedia of Integer Sequences (2019); terms a(7) through a(11) extended by Falk Hüffner, June 21, 2019. Entry definition and labeled Hamiltonian-graph counts, especially a(8) https://oeis.org/A326208
   - Also cited at Exact certificates in ham8-artifact-upward-closure and ham8-artifact-orbit-weighted-check
   - Also cited at OEIS A326208, Number of Hamiltonian labeled simple graphs with n vertices; OEIS A326207, Number of non-Hamiltonian labeled simple graphs with n vertices; OEIS A003216, Number of Hamiltonian graphs with n nodes; J. P. Dolch, Names of Hamiltonian Graphs, Congressus Numerantium 8 (1973), 259-271; Frank Harary and Edgar M. Palmer, Graphical Enumeration, Academic Press, 1973, p. 219; Brendan D. McKay and Adolfo Piperno, Practical Graph Isomorphism, II, Journal of Symbolic Computation 60 (2014), 94-112, DOI 10.1016/j.jsc.2013.09.003
   - Also cited at Inline Python 3 exact computation executed on 2026-07-24
   - reference_database; dataset source; checked 2026-08-01
   - Source use: data_used
   - Reused material: Entry definition and labeled Hamiltonian-graph counts, especially a(8)
   - Reuse basis: fair_use_reviewed; rights holder: The OEIS Foundation Inc. and the credited contributors; checked 2026-08-01; by Philip Weiss, TheoremDB staff
   - Required attribution: Gus Wiseman, “A326208: Number of Hamiltonian labeled simple graphs with n vertices,” The On-Line Encyclopedia of Integer Sequences (2019); terms a(7) through a(11) extended by Falk Hüffner, June 21, 2019.
   - For Exact Hamiltonicity probability on eight labeled vertices, this source records the exact labeled Hamiltonian-graph count used to check the eight-vertex probability.
   - Source named by the research packet.