Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant

DOI10.4230/LIPICS.ITP.2022.25MaRDI QIDQ6572563FDOQ6572563

Authors: Nicolas Magaud 

Publication date: 15 July 2024

zbMATH Keywords

projective geometrypackingsspreadsfinite modelscoqPG(3,2)

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

This page was built for publication: Proof pearl: formalizing spreads and packings of the smallest projective space PG(3,2) Using the coq proof assistant

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6572563)