论文标题
正式的PG（3,2）的传播和包装！
Spreads and Packings of PG(3,2), Formally!
论文作者
论文摘要
我们研究如何在COQ证明助理中形式化最小的投影空间PG（3,2）。然后，我们正式描述了PG（3,2）的扩展和包装及其某些特性。正式化非常简单，但是随着危险对象数量的增加，我们需要利用一些对称性参数以及智能证明技术，以使证明搜索和验证更快，因此使用COQ证明助手可以进行处理。 这项工作可以视为正式化更高维度的投射空间的第一步，例如pg（4,2）或更大的顺序，例如PG（3,3）。
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).
