英文：Mathematical Theorem Proving 分类：science
用 AI 自动或辅助证明数学定理的技术，将数学推理形式化为机器可验证的步骤序列。它分为自动定理证明（ATP）与交互式证明助手（ITP），是形式化数学与 AI4S 的前沿方向。
方法包括：搜索式证明（基于策略的强化学习，如 AlphaProof、Lean 环境）、大模型生成证明步骤（与证明助手交互）、神经-符号结合（预测下一步策略+验证）。关键组件是形式化语言（Lean、Coq）与高质量训练语料；评测用证明成功率与验证完备性。
用于数学研究辅助（竞赛题、开放猜想探索）、软件验证（形式化规范证明）与教育；IMO 金牌级成果（AlphaProof 2024）标志该方法进入实用前沿。
相关词条：AI 科学家 · AI for Science · AlphaFold · 知识图谱科学推理 · 形式化验证