← All papers
Formalising the Kruskal-Katona Theorem in Lean
cs.LO
Sep 19, 2022 · v1
TL;DR
Formalizes the Kruskal-Katona theorem and colex orderings for extremal combinatorics in Lean.
Abstract
This paper describes the formalization of the Kruskal-Katona theorem in the Lean theorem prover. The Kruskal-Katona theorem characterizes the shadow (lower shadow) of set families and is a fundamental result in extremal combinatorics. The formalization follows a proof via compressions and includes the construction of colex orderings and the Lovász form of the theorem.
Problem
The Kruskal-Katona theorem, a fundamental result in extremal combinatorics characterizing the shadow of set families, had not been formalized in a proof assistant.
Approach
The authors formalize the Kruskal-Katona theorem in Lean following a proof via compressions. The formalization includes colex orderings and the Lovasz form of the theorem.
Results
A complete machine-checked proof of the Kruskal-Katona theorem is produced in Lean, covering the compression-based argument and the equivalence with the Lovasz formulation.