Spreads and Packings of PG(3,2), Formally!

TL;DR

This paper formalizes the smallest projective space PG(3,2) in Coq, focusing on spreads and packings, and discusses techniques to handle complexity for potential extension to higher dimensions or larger spaces.

Contribution

It provides a formal Coq framework for PG(3,2), including spreads and packings, with methods to manage complexity for future formalizations of larger projective spaces.

Findings

Formalization of PG(3,2) in Coq completed

Techniques for handling combinatorial complexity developed

Foundation laid for formalizing higher-dimensional projective spaces

Abstract

We study how to formalize in the Coq proof assistant the smallest projective space PG(3,2). We then describe formally the spreads and packings of PG(3,2), as well as some of their properties. The formalization is rather straightforward, however as the number of objects at stake increases rapidly, we need to exploit some symmetry arguments as well as smart proof techniques to make proof search and verification faster and thus tractable using the Coq proof assistant. This work can be viewed as a first step towards formalizing projective spaces of higher dimension, e.g. PG(4,2), or larger order, e.g. PG(3,3).