DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.19

Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean

Authors: Eric Jonathan Wang and Elif Uskuplu

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

Abstract

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.

Cite as

Eric Jonathan Wang and Elif Uskuplu. Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.ITP.2026.19,
  author =	{Wang, Eric Jonathan and Uskuplu, Elif},
  title =	{{Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.19},
  URN =		{urn:nbn:de:0030-drops-269936},
  doi =		{10.4230/LIPIcs.ITP.2026.19},
  annote =	{Keywords: Lean theorem prover, combinatorial design theory, BIBD, matrix theory, Bruck-Ryser-Chowla theorem, quadratic forms}
}

Search Results

Documents authored by Uskuplu, Elif

Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean

Abstract

Cite as

Thanks for your feedback!

Could not send message