# 数学 · 推导与证明：AI任务边界证据

版本 2026-10-19.boundary.1；截至 2026-10-19；整理 2026-10-19

全模块16个代表任务切片；当前聚焦1个M03；不是完整职业清单或任务覆盖比例。
主轴按原始材料公开日期；实验/上线时点另列。历史空白仅表示本次未收录证据；后来的质疑不偷偷改写早期结果。
任务定义、验收和术语是今天整理的对照框架；历史筛选只约束证据公开时间，不代表这些说明在当时已经存在。
实际覆盖比例：未知（null）

## M03 为形式化命题搜索机器可检证明
输入：用逻辑语言写出的命题、库与环境版本。形式化是把问题及条件写成计算机可逐步核查的语言；Lean是这种证明检查工具。
交付：可由内核检查的证明文件
人负责：检查所写形式命题是否正是原问题，核对假设与自然语言含义
证据适配：形式化已提供命题的证明搜索；不等于自动选题及发表研究
验收：固定Lean环境重放通过；不额外假定结论，不用未完成证明占位；自然语言与形式命题一致

### 公开 2024-07-25 形式证明扩展到多种竞赛命题
证据类型：限定评测；方式：限定输入下由系统执行
当前引用状态：BM04 active · 当前可引用（不等于现场验证）。
AlphaProof完成2道代数与1道数论题；配合AlphaGeometry2，共4/6题、28/42分。
AI参与动作：人在形式化后，系统搜索证明；AlphaProof完成2道代数与1道数论题。
配置：专家先形式化；AlphaProof使用Lean；系统部分题耗时最长3天
指标：组合系统的竞赛分；不是AlphaProof单独4/6
事件/运行：精确日期未披露
日期依据：按该条支持材料的公开日期进入时间轴；不是实验统一发生日
意义：系统可搜索机器可检证明，但自然语言与形式命题的转换仍由人承担。
比较：任务/配置或指标不同，不计算统一增长率
限制：不能拿组合成绩当Lean工具通用成功率。
- [AlphaProof与AlphaGeometry 2：IMO2024](https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/)：人工形式化说明；4/6题与28/42分；公开2024-07-25；当前状态 active · 当前可引用（不等于现场验证）；4.5小时×两场是学生制度；系统耗时最长3天，不是同时间预算

### 公开 2025-04-30 开放证明模型可按预算测量
证据类型：限定评测；方式：限定输入下由系统执行
当前引用状态：BM06 active · 当前可引用（不等于现场验证）。
DeepSeek-Prover-V2-671B CoT在miniF2F-test：pass@1为61.9%，pass@32为82.4%，pass@8192为88.9%。
AI参与动作：开放模型为已形式化命题生成机器可检证明；结果随候选预算改变。
配置：671B、先生成推理步骤（CoT）；Lean 4.9.0证明检查环境；论文采用并再次修订的miniF2F-test共244题，每题最多8192候选。数学库与环境沿论文说明，本页未核对具体commit。
指标：给定样本预算下至少一份机器可检证明的题目比例
事件/运行：精确日期未披露
日期依据：按该条支持材料的公开日期进入时间轴；不是实验统一发生日
意义：证明搜索可委派给开放模型；预算与核验环境需要一起交接。
比较：任务/配置或指标不同，不计算统一增长率
限制：88.9%不是一次调用准确率；题集有修订，不与原始题集或IMO年度得分直接连线。
- [DeepSeek-Prover-V2首稿](https://arxiv.org/html/2504.21801v1)：§3及§3.1 Experimental Results；表1（671B CoT/候选预算）、表2（题目类别）；附录C题集修订。；公开2025-04-30；当前状态 active · 当前可引用（不等于现场验证）；671B CoT的88.9%为pass@8192；82.4%为pass@32，61.9%为pass@1；不是首试成功率

## 术语速查
形式化 / Lean：把问题与条件写为机器可检查的逻辑命题；Lean检查所写命题的证明，人检查它是不是原问题。
CoT / pass@k：CoT是先生成推理步骤；Pass@K表示在指定评测标准下生成K个候选，至少一个通过的题目比例。M01的答案Pass@K核对最终答案，CoT-Pass@K另由模型裁判检查过程；两者都不等于形式证明内核通过。
自然语言核对器：用模型检查候选论证的语言流程，可能漏错；与严格规则的证明内核不同。
复数标量乘法：一次复数与复数相乘的算术操作计数；不能直接当成实数乘法次数或程序运行时间。

## 方法与材料
覆盖的含义：在指定输入、环境和验收下，材料支持AI参与哪些动作；未知比例保持null。
速度的含义：证据节点之间的日历间隔、流程交接变化；指标/样本/预算不一致时，不计算能力增长率或外推一年三年。
综述用于发现任务和原始文献；每条公开主张引用原始论文/官方记录。转载及同一文献家族不累计成独立验证。
目的性选择三个领域的代表任务，不是穷尽检索或无偏职业采样；基础时间轴于2026-10-14核对，本次精选补充与证据截止2026-10-15，固定论文优先，不把动态榜排名倒填历史。
- [AlphaProof与AlphaGeometry 2：IMO2024](https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/)；公开2024-07-25；阅读2026-10-14；当前状态 active · 当前可引用（不等于现场验证）；人工形式化说明；4/6题与28/42分；4.5小时×两场是学生制度；系统耗时最长3天，不是同时间预算
- [DeepSeek-Prover-V2首稿](https://arxiv.org/html/2504.21801v1)；公开2025-04-30；阅读2026-10-14；当前状态 active · 当前可引用（不等于现场验证）；§3及§3.1 Experimental Results；表1（671B CoT/候选预算）、表2（题目类别）；附录C题集修订。；671B CoT的88.9%为pass@8192；82.4%为pass@32，61.9%为pass@1；不是首试成功率
- [数学推理综述](https://arxiv.org/html/2506.08446v1)；公开2025-06-10；阅读2026-10-14；当前状态 active · 当前可引用（不等于现场验证）；§3推理组成；§4方法；§5–6局限；综述用于任务框架与机制，不回填更早年份的已知成绩
- [自动形式化综述](https://arxiv.org/html/2505.23486v1)；公开2025-05-29；阅读2026-10-14；当前状态 active · 当前可引用（不等于现场验证）；formalization定义；评测/语义对齐讨论；机器核查形式命题不保证与自然语言原问题等价