AI4Math 综述：从引导猜想到形式化证明，AI 已能解出 PKU 研究生考题并在 Lean 中验证 Erdős 问题的反例

综述提出 AI4Math 不只是把 AI 用于数学，还包括把数学作为检验通用推理能力的试验台，并把研究划分为面向特定问题的建模与通用建模两大互补方向。 相对以往按任务或按模型罗列的综述，这里给出一个统一的概念框架：面向特定问题的建模（引导直觉、构造反例、封闭系统形式推理）与通用建模（自然语言推理、形式推理、数学信息检索），并说明二者在数据、算力与迁移性上的取舍。 这是概念性综述与分类，依据是对代表性工作的梳理与图 1 的框架图，而非新的实验数据。

作者自建 PKU 评测显示推理增强模型已能处理相当一部分研究生数学：在 11 门本科期末考题上 GPT-4 平均 59.6，o1 为 89.7、DeepSeek-R1 为 85.0、o3-mini 为 92.2、Gemini 2.5 Pro 为 94.2；o3-mini 在 58 道博士资格考试题上平均 84.4，代数最强、几何与拓扑最弱。 相对以往只报告竞赛或本科基准的结果，这里用同一套人工评分标准（0–5 分）在本科与博士两个层级上横向比较五个模型，并给出学科间的强弱差异。 100 道本科题来自 11 门课程、58 道博士题来自四个方向，由人类专家按 0–5 分标准评分；作者也提示可能存在数据污染，且考题与开放研究不同。

综述指出形式系统为 AI 提供可验证的监督信号，并记录了形式推理代理的实用成果：Aletheia 解出 FirstProof 十题中的六题，Numina-Lean-Agent 解出 2025 年 Putnam 全部题目，Aristotle 等代理参与了对 Erdős 问题（如 #205 反例、#367 部分解决）的形式化验证流程。 相对早期只做基准测试的形式证明工作，这里强调代理工作流把前沿模型的启发式输出转化为 Lean 中机器可检验的结论，从而缓解研究级数学的验证瓶颈。 依据是综述引用的具体系统与结果，包括 mathlib4 截至 2025 年 12 月含逾 25 万条定理与 12 万条定义，以及 Liquid Tensor Experiment 等里程碑；作者也说明这些 Erdős 相关案例是代表性而非定论。

综述把未来方向归纳为七点，核心是：领域专业知识与特征工程仍不可替代、验证瓶颈与自动形式化、形式化的语义一致性、从正确性走向理解、从启发式走向专家式工作流、数学家的主动参与，以及把 AI 当作研究副驾驶。 相对只谈模型能力的讨论，这里把“验证杠杆”作为论证核心：生成候选解昂贵而验证相对廉价，因此即便 AI 的推理正确率低，只要验证成本低，整体研究效率仍可提升。 这是基于前述进展的论证与展望，引用了 Thurston、Ulam 与 Georgiev 等人的观点，属于立场性论述而非实验结论。

这篇综述面向希望快速了解 AI4Math 全貌的读者，包括数学研究者、AI 研究者与工程实践者。它明确把范围限定在数学推理（发现、形式化、证明），不覆盖 AI 用于计算数学与科学计算（如 PDE、优化、反问题），并建议读者参考其他综述。文中的 PKU 评测适用于本科与博士资格考试这一设定，作者也提示考题与开放研究不同、可能存在数据污染。综述的结论适用于理解当前能力边界与研究方向，而非给出可直接套用的工程方案。

读者仍需留意几点：PKU 评测基于考试题，作者自己提示可能存在数据污染，且考试题与开放研究问题性质不同，因此分数应视为能力信号而非研究能力的直接度量。Erdős 问题相关的形式化成果被作者描述为代表性而非定论，且形式化虽能大幅降低幻觉风险，却不能消除所有失败模式，例如模型可能利用非预期的题目设定或重新发现已有文献中的论证。此外，综述对计算数学与科学计算只作提及而未展开，若读者关心 PDE、优化或反问题，需要另找资料。