定理证明是指使用严格的逻辑语言描述数学定义和数学证明，并在计算机的辅助下验证数学定理的正确性。定理证明可用于验证计算机系统的可靠性和安全性：首先将待验证的软硬件系统和需要满足的要求表达为数学命题，再利用定理证明工具检验该数学命题是否正确。相比于传统的基于测试的可靠性保障方法，定理证明技术会考虑所有边缘情况，完全排除一整类的潜在错误。 定理证明又可分为自动定理证明和交互式定理证明：

• 自动定理证明基于SAT、SMT、一阶定理证明等算法，试图自动判定逻辑命题的正确性。涉及的逻辑命题可能包含量词、未解释函数、线性和非线性算数、数组、位向量等等。自动定理证明技术在硬件和软件验证中有着广泛的应用。
• 交互式定理证明试图通过人和计算机之间的交互完成证明，其特点是需要更多的人工参与，但能验证更复杂的系统和性质。目前许多大规模的形式化验证工作都基于交互式定理证明技术，例如seL4操作系统微内核和CompCert编译器的验证。 除了在硬件、编译器、操作系统等传统领域的应用，定理证明也已经用于各种新兴领域，例如机器人、区块链、量子计算、深度学习、等等，协助确保这些领域软硬件系统的可靠性。 本网站的一个主要目标是收集与定理证明相关的各类资源，包括教程、文献和项目的链接，以便初学者和研究人员查找和使用。