Chromatic number of (0,2)-graphs

Definition\((0,2)\)-graphs#✓fully proved

For a natural number \(n\), a simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) is a \((0,2)\)-graph when every two distinct vertices of \(G\) have either exactly zero or exactly two common neighbors.

def IsZeroTwo {n : ℕ} (G : SimpleGraph (Fin n)) : Prop :=
  ∀ u v : Fin n, u ≠ v →
    (G.commonNeighbors u v).ncard = 0 ∨
      (G.commonNeighbors u v).ncard = 2

Used by 1

Used byThe three-chromatic \((0,2)\)-graph conjecture

DefinitionThe three-chromatic \((0,2)\)-graph conjecture#✓fully proved

It asserts that there are a natural number \(n\) and a simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) in which every two distinct vertices have either zero or two common neighbors, such that the chromatic number of \(G\) is \(3\).

noncomputable def conjecture : Prop :=
  ∃ (n : ℕ) (G : SimpleGraph (Fin n)),
    IsZeroTwo G ∧ G.chromaticNumber = 3

Uses 1 · Used by 1

Statement uses\((0,2)\)-graphs

Used byNo finite \((0,2)\)-graph has chromatic number three

TheoremNo finite \((0,2)\)-graph has chromatic number three#●ready to prove

For every natural number \(n\) and every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) in which every two distinct vertices have either zero or two common neighbors, the chromatic number of \(G\) is not \(3\). In particular, the three-chromatic \((0,2)\)-graph conjecture is false.

Williamson proves the stronger statement that every finite three-colourable \((0,2)\)-graph is bipartite (Theorem 2 of the source below).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Christopher Williamson, Finite Three-Colourable (0,2)-Graphs Are Bipartite, arXiv preprint (2026), arXiv:2607.10125, https://arxiv.org/abs/2607.10125.

Uses 1

Statement usesThe three-chromatic \((0,2)\)-graph conjecture

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.