Nicolas Magaud. Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3, 2) Using the Coq Proof Assistant. In June Andronick, Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel. Volume 237 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. [doi]
Abstract is missing.