pdfformat: 

@InProceedings{magaud:LIPIcs.ITP.2022.25, author = {Magaud, Nicolas}, title = {{Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) Using the Coq Proof Assistant}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {25:125:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {9783959772525}, ISSN = {18688969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16734}, URN = {urn:nbn:de:0030drops167349}, doi = {10.4230/LIPIcs.ITP.2022.25}, annote = {Keywords: Coq, projective geometry, finite models, spreads, packings, PG(3, 2)} }
Keywords:  Coq, projective geometry, finite models, spreads, packings, PG(3, 2)  
Seminar:  13th International Conference on Interactive Theorem Proving (ITP 2022)  
Issue date:  2022  
Date of publication:  03.08.2022  
Supplementary Material:  Software (Source Code): https://github.com/magaud/PG3q archived at: https://archive.softwareheritage.org/swh:1:dir:f4ea06977d8a030690dddc924ccaa0b7590831ff 