[#P2584] Exact Hamiltonicity probability on eight labeled vertices

A mathematical schematic of Exact Hamiltonicity probability on eight labeled vertices. — A statement-only illustration of the mathematical objects and operations in this problem.

Contents

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

Agent access

Definitions and notation

1Context

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

2Problem setup

Remark 1. Each of the 28 possible edges is independently present or absent.

Definition 1. A Hamilton cycle visits all eight vertices exactly once.

3What counts as a solution

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

1Resolution

What counts as a solution

Answer (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.^[2]

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

1Packet records

Show recorded summaries

Record	Kind	Assessment
The exact probability is 9,479,757 divided by 16,777,216, approximately 0.565037548542022705078125.	Result	Evidence: Reproduced A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1 The exact probability is 9,479,757 divided by 16,777,216, approximately 0.565037548542022705078125.^[2] Relevance to this problem For Exact Hamiltonicity probability on eight labeled vertices, record ham8-claim-exact-labeled-probability (“Exactly 151,676,112 labeled graphs on eight vertices are Hamiltonian”) records a bound, answer, status fact, or structural consequence. The record states: The exact probability is 9,479,757 divided by 16,777,216, approximately 0.565037548542022705078125. Evidence ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope. Record state established Scope every simple graph on the fixed labeled vertex set {0,1,2,3,4,5,6,7} Sources Reference 2 Details 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)\|\). Open full record →
A326208 gives 151,676,112, A326207 gives 116,759,344, and the classical unlabeled sequence gives 6,196 classes.	Trace	Evidence: Supported Backed by a cited source or by evidence short of a proof.
attempt · Route 1 A326208 gives 151,676,112, A326207 gives 116,759,344, and the classical unlabeled sequence gives 6,196 classes.^[2] Relevance to this problem For Exact Hamiltonicity probability on eight labeled vertices, record ham8-attempt-enumeration-table-audit (“OEIS records the labeled count and its complement”) documents a concrete method, search boundary, or failed route. The record states: A326208 gives 151,676,112, A326207 gives 116,759,344, and the classical unlabeled sequence gives 6,196 classes. Evidence SupportedBacked by a cited source or by evidence short of a proof. Record state completed Scope published and maintained enumeration records checked for Hamiltonian graphs on eight vertices in labeled and unlabeled conventions Sources Reference 2 What happened OEIS A326208 is the labeled sequence. Its \(n=8\) term is 151,676,112, and its entry says the terms from orders 7 through 11 were added using Falk Hueffner's tinygraph at version `9766535`. OEIS A326207 independently records the complementary \(n=8\) term 116,759,344. Their sum is \(2^{28}\). OEIS A003216 records the unlabeled sequence and gives 6,196 at order 8. It cites J. P. Dolch's 1973 enumeration, Harary and Palmer's 1973 book, and later graph atlases. The nauty orbit computation in this fixture reproduces both the 6,196 unlabeled term and the labeled A326208 term. The checked records settle this database target as a known finite enumeration. The two included computations supply local certificates with fixed encodings and checksums. Related: Computation 1 Open full record →
A standard-library Python program marks every Hamilton cycle, closes upward under edge addition, and hashes the full truth table.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1 A standard-library Python program marks every Hamilton cycle, closes upward under edge addition, and hashes the full truth table.^[2] Relevance to this problem For Exact Hamiltonicity probability on eight labeled vertices, record ham8-artifact-upward-closure (“Replayable 32 MiB upward-closure certificate”) supplies evidence or a replay used to check the packet. The record states: A standard-library Python program marks every Hamilton cycle, closes upward under edge addition, and hashes the full truth table. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope the complete 2^28-bit truth table for Hamiltonicity on eight labeled vertices, with smaller-order regression checks for 3 <= n <= 7 Sources Reference 2 Entry point `Join source_lines with newline characters, save as check.py, and run python3 check.py` Runtime Python 3.6 or later, standard library only Details Index the 28 edges lexicographically and identify each labeled graph with its 28-bit edge mask. Fix vertex 0 at the start of a cycle and retain one orientation. This produces \((8-1)!/2=2{,}520\) distinct Hamilton-cycle masks. The seed bitset has a 1 at each cycle mask. For edge bit \(e\), `lower_half_mask` selects graph-mask indices whose \(e\)-th bit is zero. The assignment ``` closure \|= (closure & lower_half_mask) << (1 << e) ``` adds that edge to every currently marked graph that lacks it. After all 28 passes, a position is marked exactly when its edge set contains one of the Hamilton-cycle masks. Bits are packed little-endian within bytes, with graph mask \(m\) at byte `m // 8`, bit `m % 8`. The 32 MiB closure has SHA-256 digest `11a753fc14644c902b0917d28ced9aa0fa419078514f97b8b7942daac19ff946`. Its edge-count histogram agrees entry by entry with the orbit-weighted computation. The same program reproduces the candidate's counts \(1,10,218,10078,896756\) at orders 3 through 7. Related: Computation 1 Open full record →
An isomorph-free generator and automorphism-group calculation give the same labeled total and edge histogram.	Artifact	Evidence: Executable material Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 2 An isomorph-free generator and automorphism-group calculation give the same labeled total and edge histogram.^[1] Relevance to this problem For Exact Hamiltonicity probability on eight labeled vertices, record ham8-artifact-orbit-weighted-check (“Independent nauty orbit-weighted enumeration”) supplies evidence or a replay used to check the packet. The record states: An isomorph-free generator and automorphism-group calculation give the same labeled total and edge histogram. Evidence Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay. Record state available Scope all isomorphism classes of simple graphs on eight vertices, generated once each and weighted by 8!/\|Aut(G)\| Sources Reference 1 Entry point `Compile source_lines as orbit_check.cc against tinygraph Graph.o, Set.o, geng.o and its nauty 2.6r6 objects, then run the resulting executable` Runtime C++11, tinygraph commit 97665350689943d64b90ca1501b3291db0538a0a, and nauty 2.6r6 Details This check uses tinygraph at commit `97665350689943d64b90ca1501b3291db0538a0a`, the version cited by OEIS A326208, together with nauty 2.6r6. `Graph::enumerate(8, ...)` supplies one representative of every isomorphism class. A separate depth-first search tests for a Hamilton cycle while fixing vertex 0 as the start. For each passing representative \(G\), nauty computes \(\|\operatorname{Aut}(G)\|\), and `numLabeledGraphs()` returns \(8!/\|\operatorname{Aut}(G)\|\). There are 6,196 passing representatives among all 12,346 classes. Their weights sum to 151,676,112. The labeled edge histogram matches the upward-closure histogram at every edge count. Sorted pairs of graph6 records and little-endian orbit weights have FNV-1a fingerprint `16813842364046026506`. Related: Computation 1 · Artifact 1 Open full record →
No records match these filters.

Notes and companion material

Original intake status. SOLVED in the independently reviewed TheoremDB packet as of 2026-08-01. The exact probability is 9,479,757 divided by 16,777,216, approximately 0.565037548542022705078125.

Independent isolated execution completed successfully for Replayable 32 MiB upward-closure certificate, Independent nauty orbit-weighted enumeration. Every embedded assertion passed and the run reproduced the selected exact result: The exact probability is 9,479,757 divided by 16,777,216, approximately 0.565037548542022705078125.
Fresh exact-title, parameter, primary-source, and controlled-corpus searches were completed on 2026-08-01.

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

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.

How the 4 records connect

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemExact Hamiltonicity probability on eight labeled vertices

All 4 recorded relations between these records and the problem

2See also

Median satisfiability threshold for a six-variable clause setprobabilistic combinatorics
Rank log-concavity for symmetric binary matrices through order fiftyprobabilistic combinatorics
A period-six recurrence for domination on the three-row knight graphgraph theory

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Exact Hamiltonicity probability on eight labeled vertices.” TheoremDB. P2584. Problem statement; statement text SHA-256 f40f9bbbafc5509afda05561f3507e8d6b309bba0fceeab21ec44e9d593d2e9a. https://theoremdb.org/statement/?ref=P2584

BibTeX

@misc{theoremdb-problem-f40f9bbbafc5509afda05561f3507e8d6b309bba0fceeab21ec44e9d593d2e9a,
  title = {{Exact Hamiltonicity probability on eight labeled vertices}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 f40f9bbbafc5509afda05561f3507e8d6b309bba0fceeab21ec44e9d593d2e9a},
  url = {https://theoremdb.org/statement/?ref=P2584}
}

Plain text: Built Markdown snapshot

This problem includes 4 records joined by 4 typed links, sourced from oeis.org^[2], current as of July 24, 2026.

1Lean verification

Lean formalization needed

An informal proof is recorded. No Lean formalization is attached.

Open TheoremDB Researcher

Upload a Lean project archive

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.

1References

Falk Hüffner, tinygraph: Exploring Graph Conjectures on Small Graphs, GitHub repository, commit 97665350689943d64b90ca1501b3291db0538a0a, May 8, 2019. Independent C++11 driver executed against tinygraph 9766535 and nauty 2.6r6 on 2026-07-24. ↗software · software source · pinned repository version in URL · checked 2026-08-01Source use: original summary.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.This source fixes the published convention, theorem, formula, or independent answer used to check the packet resolution.Also cited at pinned commit 9766535, graph-enumeration and Hamiltonicity routines invoked by the independent C++11 driver.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.
Packet source. 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). ↗reference database · dataset source · checked 2026-08-01Source 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.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.Source named by the research packet.

Finite exact probability target with a direct 2^28 truth table and a compact cycle-mask representation.

Discussion

Loading discussion.

[#P2584] Exact Hamiltonicity probability on eight labeled vertices

1Context

2Problem setup

3What counts as a solution

1Resolution

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Context

2Problem setup

3What counts as a solution

1ResolutionResolvedNot Lean-verified

1Packet records

Recent contributions

Computational notes

2See also

1Lean verification

What the formal work covers

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance

1Resolution