自动定理证明（Automated Theorem Proving，ATP）是计算机科学与数学逻辑的交叉研究领域，旨在通过计算机程序自动推导并验证数学命题或逻辑公式的正确性。其核心方法包括归结原理、模型检验、交互式证明辅助等，代表系统有Coq、Lean、Isabelle等。广泛应用于形式化数学、程序正确性验证及硬件逻辑验证等领域。