Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Proof of `Six color theorem`

groundedproofs/Lax909950Proofs/SixColoring.lean · lax-909950

What this proof establishes

thm✓Lax909950.SixColoring

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

In the paper

  • page 2 of this submission's paper

Description

By induction on the number of vertices: remove a vertex of degree at most 55, color the remaining graph, and give the removed vertex a color not used by any of its neighbors.