论文标题
正式化Fisher的不平等：组合制剂中的正式线性代数证明技术
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
论文作者
论文摘要
数学的形式化持续迅速，但是组合主义者继续对形式化的努力提出挑战，例如它依赖数学领域其他广泛领域的技术。本文介绍了正式的线性代数技术，以证明Isabelle/HOL的发病率结构，以及它们在Fisher不平等的首次形式化中的应用。除了对线性代数表示推理的正式发病率矩阵和简单技术外，正式化还集中在线性代数结合和等级参数上。正如我们通过进一步的应用来证明费舍尔不平等的差异证明，这些技术可以很容易地适应将来的组合形式化。
The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wide range of other fields in mathematics. This paper presents formal linear algebraic techniques for proofs on incidence structures in Isabelle/HOL, and their application to the first formalisation of Fisher's inequality. In addition to formalising incidence matrices and simple techniques for reasoning on linear algebraic representations, the formalisation focuses on the linear algebra bound and rank arguments. These techniques can easily be adapted for future formalisations in combinatorics, as we demonstrate through further application to proofs of variations on Fisher's inequality.
