  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).
