Paper I: a finite, Lean-verified fractional clique-partition bound for split graphs. Part of an Erdős #81 research program; #81 remains open.
graph-theory formal-verification mathlib lean4 chordal-graphs erdos-problems extremal-combinatorics split-graphs clique-partition triangle-packing
-
Updated
Jul 9, 2026 - Lean