Lax Lean Archive

Barnette's Conjecture

lax-881656·formalized by Clemens Kuske·registered·created ·GitHub @2ba3548·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    Barnette's conjecture asserts that every finite, simple, cubic, bipartite, planar, 3-connected graph has a Hamiltonian cycle. It remains one of the central open problems about Hamiltonicity in planar graphs.

    This submission presents the conjecture as an open theorem statement over finite simple graphs. Four separate definition concepts introduce 3-connected graphs, cubic graphs, bipartite graphs, and Hamiltonian cycles. Planarity is deliberately not duplicated: the conjecture imports the straight-line-drawing predicate from the Planar Graph Classes submission. No proof is supplied.

    Recent progress proves the conjecture for Barnette graphs whose faces all have size at most eight. Maximum face size ten is the next natural restricted case.

    Concepts

    Concept map
    8 concepts
    100%
    Open claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    No proofs in this submission.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-881656,
  author = {Clemens Kuske},
  title = {Barnette's Conjecture},
  year = {2026},
  howpublished = {Lax Archive, lax-881656},
  url = {https://laxarchive.org/lax-881656/},
}

    References

    1. Tobias Schnieders. Barnette Graphs with Faces up to Size 8 are Hamiltonian. 2025. doi:10.48550/arXiv.2508.03531 · arXiv:2508.03531

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…