Lax Lean Archive

Barnette's conjecture

Lax881656.BarnetteConjecture · concepts/Lax881656/BarnetteConjecture.lean · lax-881656

open

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this concept

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

    No source line selected.

    Natural Language Statement

    Opn

    Every finite, simple, 3-connected, cubic, bipartite planar graph has a Hamiltonian cycle.

    This is an open problem. The conjecture is known when every face has size at most 8; maximum face size 10 is the next natural restricted case.

    Concept map
    8 concepts
    100%
    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    No proof in the archive yet — this claim is open.

    Lean source view on GitHub

    1import Lax68.Planar
    2import Lax881656.ThreeConnected
    3import Lax881656.Cubic
    4import Lax881656.Bipartite
    5import Lax881656.HamiltonianCycle
    6
    7/-!
    8---
    9title: Barnette's conjecture
    10type: opn
    11---
    12Every finite, simple, 3-connected, cubic, bipartite planar graph has a
    13Hamiltonian cycle.
    14
    15This is an open problem. The conjecture is known when every face has size at
    16most 8; maximum face size 10 is the next natural restricted case.
    17
    18# Formalization notes
    19
    20Finite simple graphs are stated on the canonical vertex type `Fin n`.
    21Planarity is the straight-line-drawing predicate imported from the Planar
    22Graph Classes submission; the other four hypotheses and conclusion use the
    23dedicated definition concepts in this submission.
    24-/
    25
    26set_option autoImplicit false
    27
    28namespace Lax881656.BarnetteConjecture
    29
    30/-- Barnette's conjecture: every 3-connected cubic bipartite planar graph has
    31a Hamiltonian cycle. -/
    32axiom barnette_conjecture {n : ℕ} (G : SimpleGraph (Fin n)) :
    33 (Lax881656.ThreeConnected.IsThreeConnected G ∧
    34 Lax881656.Cubic.IsCubic G ∧
    35 Lax881656.Bipartite.IsBipartite G ∧
    36 Lax68.Planar.IsPlanar G) →
    37 Lax881656.HamiltonianCycle.HasHamiltonianCycle G
    38
    39end Lax881656.BarnetteConjecture
    40
    Formalization notes

    Finite simple graphs are stated on the canonical vertex type FinnFin n. Planarity is the straight-line-drawing predicate imported from the Planar Graph Classes submission; the other four hypotheses and conclusion use the dedicated definition concepts in this submission.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…