Baranyai's theorem on factorisations of complete uniform hypergraphs, formalised in Lean 4 with Mathlib

Abstract

For positive integers $n,k$, Baranyai's theorem (1975) says that if $k$ divides $n$, the $\binom nk$ $k$-element subsets of an$n$-element set can be split into $\binom{n-1}{k-1}$ classes, each of which is a partition of the$n$-set into $n/k$ blocks. For $k=2$ this is the classical 1-factorisation of the complete graph$K_n$, $n$ even. We describe a Lean~4 formalisation, built on Mathlib, of the theorem for vertexset $\{0,\dots,n-1\}$ (the formal colouring statement also admits $n=0$, where it holds onlyvacuously), together with its transport to an arbitrary finite type (and to theelements of a \lean{Finset}) and, for $n>0$, a partition form that spells out the disjointness,covering and class-size properties of the colour classes: each class has $n/k$ blocks (a divisionlemma that needs $k>0$), and the number of classes satisfies $\binom{n-1}{k-1}=\binom nk/(n/k)$ (anidentity that needs $n>0$, $k>0$ and $k\mid n$, and fails for $n=0$, $k=1$). The proof is Baranyai's vertex-by-vertex induction in the formgiven by Brouwer and Schrijver; the integral rounding step is obtained from Mathlib's Hall marriagetheorem, with Hall's condition derived by a weighted double count, so no integral-flow theorem isneeded. A converse shows that $k\mid n$ is necessary as soon as one colour class is a perfectmatching. The library has 617 lines in three files, contains no \lean{sorry}, and its 32 checkeddeclarations use only Lean's three standard axioms. As far as we could determine, within the searchscope described in Section 7, no earlier formal proof of the theorem was public.