Lax Lean Archive

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

Proof of `Planar graphs have a vertex of degree at most 5`

groundedproofs/Lax909950Proofs/LowDegree.lean · lax-909950

What this proof establishes

thm✓Lax909950.LowDegree

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

If every vertex had degree at least 66, the degree sum 2e2e would be at least 6v6v, contradicting the edge density bound e≤3v−6e \leq 3v - 6. Graphs with at most 66 vertices are handled directly.