∑ Math Proof Playground › WOWII › 65

WOWII Graph Conjecture 65

A complete machine-checked proof of the exact current Formal Conjectures theorem.

sorry-free Lean 4proof archived in CRLupstream PR #4441

Theorem

distMin(G,A) + ⌈distMin(G,M)/3⌉ ≤ largestInducedForestSize(G)

Proof idea

  1. Every nonempty proper vertex set in a connected graph has a boundary edge, so its minimum outside distance is at most one.
  2. The minimum- and maximum-degree vertex sets are nonempty, so the left side is at most two.
  3. Every nontrivial connected graph contains an induced two-vertex forest.

Artifacts

CRL proof archive.