Formal target: Corpus.Barnette.conjecture

Let G be a finite simple graph. Suppose every vertex has degree 3, its vertices can be split into two classes with every edge crossing between the classes, it can be drawn in the plane without crossing edges, and it is 3-connected: it has more than three vertices and stays connected after deleting any zero, one or two vertices. Must G have a cycle that visits every vertex exactly once before returning to its start?

Exact formal statement

∀ {V : Type} [inst : Fintype.{0} V] [inst_1 : DecidableEq.{1} V] (G : SimpleGraph.{0} V)
  [inst_2 : DecidableRel.{1, 1} (SimpleGraph.Adj.{0} G)],
  Corpus.Barnette.IsThreeConnected G →
    SimpleGraph.IsRegularOfDegree.{0} G 3 →
      SimpleGraph.IsBipartite.{0} G → Corpus.Barnette.IsPlanar G → SimpleGraph.IsHamiltonian.{0} G

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record