We present a formalization of combinatorial design theory in Lean 4, with a focus on balanced incomplete block designs (BIBDs) and their algebraic properties. The flagship result is the Bruck-Ryser-Chowla theorem, which gives the best known necessary conditions for the existence of a symmetric BIBD, formalized here in a proof assistant for the first time. Reaching this result required us to develop substantial infrastructure beyond combinatorics: we formalize Witt’s cancellation theorem for quadratic forms, prove new results on matrix congruence and block matrices, and extend Mathlib’s linear algebra library in several directions. We also provide the first formalization of Fisher’s inequality in Lean and the first formalization of the Kramer-Mesner theorem in any proof assistant, along with a reusable double-counting argument that supports standard combinatorial reasoning. The cross-domain nature of these contributions reflects a distinctive feature of design theory itself: it draws on and feeds back into many areas of mathematics, making it a particularly rewarding target for formalization within a large-scale library like Mathlib.

Abstract This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory, such as Agda. The difference from prior works is that these proofs do not assume any abuse of notation, providing more direct formalization. Also, some new notions, such as function extensionality for cofibrant exo-types, are introduced. The necessity of such notions arises during the task of formalization. In addition, we provide some novel results about inductive types using cofibrant exo-nat, the natural number type at the non-fibrant level. While emphasizing the necessity of this axiom by citing new applications as justifications, we also touch upon the semantic aspect of the theory by presenting various models that satisfy this axiom.