AI 定理证明论文精选

阅读 AI 定理证明论文，可以先选证明环境，再确定评测问题。本精选覆盖 Lean 前提检索、形式化数学基准、利用验证反馈的证明搜索与高阶逻辑。下面四篇入门论文按这些差异选择，不按分数排名，也不声称覆盖最新系统。

要搭建 Lean 证明器，先读 LeanDojo（2023）。它提供证明数据抽取和程序化交互工具，ReProver 先检索前提，再生成 tactic。发布的基准包含 98,734 条定理及证明。重点看 novel-premises 划分：依赖熟悉数学库前提的题目做得好，未必代表模型能处理训练时没用过的前提。

要比较形式化数学成绩，先读 miniF2F（2021）。它整理了来自竞赛及教学数学的 488 条形式化题目，并提供多个证明助手的版本。它是评测资源，不是证明器。比较论文百分比前，核对证明助手、验证集与测试集划分、可用 tactic 和尝试次数，不能只看题库名字相同。

要研究验证反馈如何用于训练和搜索，读 DeepSeek-Prover-V1.5（2024）。它将监督微调、强化学习和蒙特卡洛树搜索用于 Lean 4 证明生成。复现时把模型能力与搜索程序分开记录：大量尝试后找到证明，与单次生成成功，对部署成本的含义不同。保留搜索预算和验证环境，才能解释结果。

想比较另一套证明环境，读 HOList（2019）。它把 HOL Light 高阶逻辑证明整理成机器学习交互环境与基准，适合检查方法结论是否依赖 Lean 工具链。在 HOL Light 有效的方法，迁移到 Lean 后仍需验证；数学库、证明状态和动作空间都可能不同。

第一次做可复现实验，建议先用 miniF2F 理解评测约定，再用 LeanDojo 理解检索与环境接口，最后读 DeepSeek-Prover-V1.5 的反馈和搜索方案。比较证明助手生态时穿插阅读 HOList。下方解读均链接原论文，便于继续查实现和实验条件。

选系统前记录证明助手及版本、训练数据重叠、超时、尝试次数，以及最终证明是否由助手核验。这些是选择依据，不能压缩成一个通用排行榜。核验通过对应的是输入的形式化命题；形式化命题是否准确表达原本的数学问题，仍要单独检查。