证据时间轴 · 三领域试点

为形式化命题搜索机器可检证明：证据与交接

输入：用逻辑语言写出的命题、库与环境版本。形式化是把问题及条件写成计算机可逐步核查的语言；Lean是这种证明检查工具。。交付：可由内核检查的证明文件。

证据截止

2026-10-19

本次收录的公开节点

2 条

数值答案、几何构造、机器可检证明和自然语言研究证明需要不同验收；竞赛突破不能代表整个数学职业。
1个代表任务切片；实际覆盖比例未知。节点数不是覆盖率或进步次数。

●限定评测　◇产品流程　■工作实验　◆研究案例　△反例/测量受限。类型没有统一高低排名；同一任务允许同时有正面结果与限制。

任务定义、验收和术语是今天整理的对照框架；历史筛选只约束证据公开时间，不代表这些说明在当时已经存在。

公开、观察与整理，是三种时间

只画已公开节点；实验窗口仅在原文给出月份时示意。整理日不是能力发生日；靠近的公开点上下错开方便选择，纵向位置不表示能力高低。

形式证明扩展到多种竞赛命题

材料公开: 2024-07-25
实验 / 观察: 原文未给具体运行日期
本次整理: 2026-10-19；不替代运行或公开日期

开放证明模型可按预算测量

材料公开: 2025-04-30
实验 / 观察: 原文未给具体运行日期
本次整理: 2026-10-19；不替代运行或公开日期

当前证据截止 2026-10-19。月份范围不是每天的连续测量；没有实验日期的条目保持未知，不在观察轨制造点。

悬浮或键盘聚焦坐标点，先看核心信息；点击点位卡片，在详情区继续阅读。完整材料保留在下方。

先读懂这些词 · 术语速查

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

M03

为形式化命题搜索机器可检证明 ↘

● 限定评测

开放模型为已形式化命题生成机器可检证明；结果随候选预算改变。

最近材料 2025-04-30 · 限定输入下由系统执行

人：检查所写形式命题是否正是原问题，核对假设与自然语言含义

卡片标签表示最近公开材料的性质，不是这个任务整体已能自动完成；历史能力并不因后来的限制记录被删除。

怎样读这个时间轴

主轴按原始材料公开日期；实验/上线时点另列。历史空白仅表示本次未收录证据；后来的质疑不偷偷改写早期结果。

覆盖的含义：在指定输入、环境和验收下，材料支持AI参与哪些动作；未知比例保持null。

速度的含义：证据节点之间的日历间隔、流程交接变化；指标/样本/预算不一致时，不计算能力增长率或外推一年三年。

目的性选择三个领域的代表任务，不是穷尽检索或无偏职业采样；基础时间轴于2026-10-14核对，本次精选补充与证据截止2026-10-15，固定论文优先，不把动态榜排名倒填历史。

每个任务保留人的核验与决策；材料数量不等于独立实验数量，模型、Agent框架、重试预算和完整验收一并阅读。历史研究今天读取，不是当时保存的逐日网络档案。

逐项可查

任务、条件与原始证据

领域概念与前沿 →

任务切片 M03

为形式化命题搜索机器可检证明

输入: 用逻辑语言写出的命题、库与环境版本。形式化是把问题及条件写成计算机可逐步核查的语言；Lean是这种证明检查工具。
交付: 可由内核检查的证明文件
人继续负责: 检查所写形式命题是否正是原问题，核对假设与自然语言含义
证据适配: 形式化已提供命题的证明搜索；不等于自动选题及发表研究

任务验收：固定Lean环境重放通过；不额外假定结论，不用未完成证明占位；自然语言与形式命题一致。

公开 2024-07-25 · 组合系统的竞赛分；不是AlphaProof单独4/6

形式证明扩展到多种竞赛命题

AlphaProof完成2道代数与1道数论题；配合AlphaGeometry2，共4/6题、28/42分。

工作含义：系统可搜索机器可检证明，但自然语言与形式命题的转换仍由人承担。；依据：AlphaProof与AlphaGeometry 2：IMO2024

公开 2024-07-25● 限定评测

形式证明扩展到多种竞赛命题

AlphaProof完成2道代数与1道数论题；配合AlphaGeometry2，共4/6题、28/42分。

配置 / 输入: 专家先形式化；AlphaProof使用Lean；系统部分题耗时最长3天
衡量什么: 组合系统的竞赛分；不是AlphaProof单独4/6
事件 / 运行: 原文未给精确运行日期；上方为材料公开日
对任务意味着: 系统可搜索机器可检证明，但自然语言与形式命题的转换仍由人承担。
比较条件: 任务/配置或指标不同，不计算统一增长率
限制: 不能拿组合成绩当Lean工具通用成功率。

AlphaProof与AlphaGeometry 2：IMO2024 ↘

公开 2025-04-30 · 给定样本预算下至少一份机器可检证明的题目比例

开放证明模型可按预算测量

DeepSeek-Prover-V2-671B CoT在miniF2F-test：pass@1为61.9%，pass@32为82.4%，pass@8192为88.9%。

工作含义：证明搜索可委派给开放模型；预算与核验环境需要一起交接。；依据：DeepSeek-Prover-V2首稿

公开 2025-04-30● 限定评测

开放证明模型可按预算测量

DeepSeek-Prover-V2-671B CoT在miniF2F-test：pass@1为61.9%，pass@32为82.4%，pass@8192为88.9%。

配置 / 输入: 671B、先生成推理步骤（CoT）；Lean 4.9.0证明检查环境；论文采用并再次修订的miniF2F-test共244题，每题最多8192候选。数学库与环境沿论文说明，本页未核对具体commit。
衡量什么: 给定样本预算下至少一份机器可检证明的题目比例
事件 / 运行: 原文未给精确运行日期；上方为材料公开日
对任务意味着: 证明搜索可委派给开放模型；预算与核验环境需要一起交接。
比较条件: 任务/配置或指标不同，不计算统一增长率
限制: 88.9%不是一次调用准确率；题集有修订，不与原始题集或IMO年度得分直接连线。

DeepSeek-Prover-V2首稿 ↘