PG(3,2)的散布与填充的形式化！
计算机科学中的逻辑
2022-01-04 v1 符号计算
摘要
我们研究如何在Coq证明助手中形式化最小射影空间PG(3,2)。随后我们形式化描述了PG(3,2)的散布与填充，以及它们的一些性质。该形式化相当直接，但由于所涉对象数量迅速增长，我们需要利用某些对称性论证以及巧妙的证明技术，以使证明搜索与验证更快，从而在使用Coq证明助手时可行。本工作可视为迈向形式化更高维（如PG(4,2)）或更大阶（如PG(3,3)）射影空间的第一步。
引用
@article{arxiv.2201.00541,
title = {Spreads and Packings of PG(3,2), Formally!},
author = {Nicolas Magaud},
journal= {arXiv preprint arXiv:2201.00541},
year = {2022}
}
备注
In Proceedings ADG 2021, arXiv:2112.14770