# P2584: Exact Hamiltonicity probability on eight labeled vertices

- ID: `P2584`
- Reference: `hamiltonian-graph-probability-eight`
- Page: https://theoremdb.org/statements/P2584
- Export scope: built Markdown snapshot. The current public packet may have changed since this build.
- Build source revision: b5a83bd9bdbf7dfdc7134c15b7360f889389e7bc
- Current Markdown: https://api.theoremdb.org/v1/statements/hamiltonian-graph-probability-eight?representation=markdown
- Record maturity: Reviewed problem with recorded work

## The 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.

## Resolution

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

**Recorded scope.** every simple graph on the fixed labeled vertex set {0,1,2,3,4,5,6,7}

[Read this exact record and its supporting evidence](/records/ham8-claim-exact-labeled-probability)


**Resolution status:** Resolved.

**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)|\).

## Research packet

### 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** (executable material): 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** (executable material): 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. No Lean formalization is 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%0AInspect%20the%20current%20formalization%20records%20and%20verification%20history%20first.%20Continue%20an%20active%20request%2C%20draft%20check%2C%20or%20proof%20run%20when%20one%20exists%2C%20and%20avoid%20creating%20a%20duplicate%20submission.%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20needs%20work%2C%20follow%20the%20returned%20next%20step%20to%20record%20one%20Lean-shaped%20target%20draft.%20Preflight%20must%20confirm%20compilation%20before%20proof%20submission.%0A%0AChoose%20lean-proof-term-v1%20for%20a%20proof%20block%20with%20optional%20supporting_source.%20Choose%20lean-complete-file-v1%20for%20an%20existing%20complete%20file%20and%20send%20it%20unchanged%20in%20source%2C%20including%20imports.%20When%20the%20proof%20has%20local%20modules%20or%20certificate%20files%2C%20call%20createLeanProjectUpload%2C%20upload%20the%20returned%20private%20object%2C%20and%20call%20completeLeanProjectUpload.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20for%20kernel_accepted.%20Repair%20kernel%20diagnostics%20before%20submitting.%20If%20target%20correspondence%20rejects%20the%20formal%20statement%2C%20follow%20its%20repairs%20and%20check%20the%20corrected%20target%20again.%0A%0AOnce%20kernel_accepted%20is%20true%2C%20call%20submitLeanProof%20with%20that%20exact%20draft_run_id%20to%20save%20my%20submission%20request%2C%20even%20while%20target%20correspondence%20is%20pending.%20The%20saved%20request%20continues%20automatically%20after%20correspondence%20approval.%20A%20private%20check%20alone%20stays%20private.%0A%0APoll%20getLeanProofRun%20with%20the%20returned%20run_id.%20Report%20pending%20target%20review%2C%20signed%20verification%2C%20and%20packet%20attachment%20separately.%20Follow%20any%20operator-recovery%20instruction%20or%20relation-review%20handoff.%20Use%20cancelLeanProofSubmission%20only%20if%20I%20ask%20to%20withdraw%20a%20waiting%20request.).

Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.

## 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.