Document Open Access Logo

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

Authors Eric Jonathan Wang , Elif Uskuplu

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.19.pdf
  • Filesize: 0.83 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Formal software verification
Keywords
  • Lean theorem prover
  • combinatorial design theory
  • BIBD
  • matrix theory
  • Bruck-Ryser-Chowla theorem
  • quadratic forms

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.ITP.2026.19

Author Details

Eric Jonathan Wang
  • Carnegie Mellon University, Pittsburgh, PA, USA
Elif Uskuplu
  • Indiana University, Bloomington, IN, USA

Funding

Our research was conducted at the 2025 Indiana University REU program supported by NSF grant DMS-2447563. The first author acknowledges travel support from the Hoskinson Center for Formal Mathematics.

Acknowledgements

We thank Lean’s Zulip chat for answering our questions, as well as our anonymous referees for their thorough comments.

Supplementary Materials

References

  1. Aaron Anderson, Mantas Bakšys, Jonas Bayer, Mauricio Collares, Rémy Degenne, Yaël Dillies, Ben Eltschig, Sébastien Gouëzel, Kalle Kytölä, Rob Lewis, Paul Lez, Luccioli Lorenzo, Heather Macbeth, Patrick Massot, Arend Mellendijk, Kyle Miller, Pietro Monticone, Kim Morrison, Oliver Nash, Utensil Song, Terence Tao, Floris van Doorn, Sky Wilshaw, and Lawrence Wu. Formalization of the Polynomial Freiman-Ruzsa Conjecture of Marton, November 2023. URL: https://github.com/teorth/pfr.
  2. Anton Betten, Adalbert Kerber, Axel Kohnert, Reinhard Laue, and Alfred Wassermann. The discovery of simple 7-designs with automorphism group pγl(2, 32). In Gérard Cohen, Marc Giusti, and Teo Mora, editors, Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, pages 131-145, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-60114-7_10.
  3. Kevin Buzzard and Richard Taylor. The fermat’s last theorem project, 2024. URL: https://leanprover-community.github.io/blog/posts/FLT-announcement/.
  4. William G. Cochran and Gertrude M. Cox. Experimental Designs. John Wiley & Sons, New York, 2nd edition, 1957. Google Scholar
  5. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In 28th International Conference on Automated Deduction, pages 625-635. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  6. Chelsea Edmonds and Lawrence C. Paulson. Combinatorial design theory. Archive of Formal Proofs, 2021. , Formal proof development. URL: https://isa-afp.org/entries/Design_Theory.html.
  7. Chelsea Edmonds and Lawrence C. Paulson. A modular first formalisation of combinatorial design theory. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics, pages 3-18, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-81097-9_1.
  8. Chelsea Edmonds and Lawrence C. Paulson. Fisher’s inequality: Linear algebraic proof techniques for combinatorics. Arch. Formal Proofs, 2022, 2022. URL: https://www.isa-afp.org/entries/Fishers_Inequality.html.
  9. Chelsea Louise Edmonds. Formalising Combinatorial Structures and Proof Techniques in Isabelle/HOL. PhD thesis, University of Cambridge, September 2023. Google Scholar
  10. Ronald A. Fisher. The Design of Experiments. Oliver and Boyd, Edinburgh, 1935. Google Scholar
  11. Sarah J. Johnson and Steven R. Weller. A family of irregular LDPC codes with low encoding complexity. IEEE Communications Letters, 7(2):79-81, 2003. URL: https://doi.org/10.1109/LCOMM.2002.808375.
  12. E. F. Assmus Jr. and J. D. Key. Designs and Their Codes, volume 103 of Cambridge Tracts in Mathematics. Cambridge University Press, 1992. Google Scholar
  13. Michael Kiermaier, Vedran Krčadinac, Vladimir D. Tonchev, Renata Vlahović Kruc, and Alfred Wassermann. Some new Steiner designs S(2,6,91). Journal of Algebraic Combinatorics, 62:article no. 38, 2025. URL: https://doi.org/10.1007/s10801-025-01468-6.
  14. Earl S. Kramer and Dale M. Mesner. t-designs on hypergraphs. Discrete Mathematics, 15(3):263-296, 1976. URL: https://doi.org/10.1016/0012-365X(76)90030-3.
  15. Tsit-Yuen Lam. Introduction to Quadratic Forms over Fields, volume 67 of Graduate Studies in Mathematics. American Mathematical Society, Providence, RI, 2005. Google Scholar
  16. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, January 2020. URL: https://doi.org/10.1145/3372885.3373824.
  17. Herbert John Ryser. The existence of symmetric block designs. Journal of Combinatorial Theory, Series A, 32:103-105, 1982. URL: https://doi.org/10.1016/0097-3165(82)90068-1.
  18. D. R. Stinson. Universal hashing and authentication codes. In Joan Feigenbaum, editor, Advances in Cryptology - CRYPTO '91, pages 74-85, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg. Google Scholar
  19. Douglas R. Stinson. Combinatorial Designs: Constructions and Analysis. Springer, New York, 2004. Google Scholar
  20. Douglas R. Stinson. Combinatorial designs and cryptography, revisited. In 50 Years of Combinatorics, Graph Theory, and Computing, pages 335-358. CRC Press, 2020. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact