数值推导：先确定你要验收哪种正确 →
得到对的数字，不一定给出了成立的推导。先区分答案、推理步骤和形式证明，再选择核验方法。
证据时间轴 · 三领域试点
拖动时间，看AI走进哪些具体任务
从代码片段到待审代码变更（PR），从数字答案到可检查证明，从财报问答到多步金融研究。每一个变化，都回到它的任务、条件和原始材料。
证据截止
2026-10-19本次收录的公开节点
12 条数值答案、几何构造、机器可检证明和自然语言研究证明需要不同验收；竞赛突破不能代表整个数学职业。
6个代表任务切片；实际覆盖比例未知。节点数不是覆盖率或进步次数。
●限定评测 ◇产品流程 ■工作实验 ◆研究案例 △反例/测量受限。类型没有统一高低排名；同一任务允许同时有正面结果与限制。
任务定义、验收和术语是今天整理的对照框架；历史筛选只约束证据公开时间，不代表这些说明在当时已经存在。
悬浮或键盘聚焦坐标点，先看核心信息；点击点位卡片，在详情区继续阅读。完整材料保留在下方。
先读懂这些词 · 术语速查
- 形式化 / Lean
- 把问题与条件写为机器可检查的逻辑命题；Lean检查所写命题的证明，人检查它是不是原问题。
- CoT / pass@k
- CoT是先生成推理步骤；Pass@K表示在指定评测标准下生成K个候选，至少一个通过的题目比例。M01的答案Pass@K核对最终答案，CoT-Pass@K另由模型裁判检查过程；两者都不等于形式证明内核通过。
- 自然语言核对器
- 用模型检查候选论证的语言流程，可能漏错；与严格规则的证明内核不同。
- 复数标量乘法
- 一次复数与复数相乘的算术操作计数；不能直接当成实数乘法次数或程序运行时间。
聚焦一项任务，准备交接与验收
M01
写出多步数值问题的推导 ↘
● 限定评测通过重复采样寻找正确答案；每次尝试与推理正确性需要另外核验。
最近材料 2025-11-24 · 人机协作人：核对单位、条件与每一步理由
M02
构造并检查几何证明 ↘
● 限定评测系统提出辅助构造并用符号引擎推演；限定30题中完成25题。
最近材料 2024-01-17 · 限定输入下由系统执行人：核对形式表达、图形假设与推广
M03
为形式化命题搜索机器可检证明 ↘
● 限定评测开放模型为已形式化命题生成机器可检证明；结果随候选预算改变。
最近材料 2025-04-30 · 限定输入下由系统执行人：检查所写形式命题是否正是原问题，核对假设与自然语言含义
M04
起草自然语言的高难度证明 ↘
● 限定评测特定研究版本直接接自然语言题目并输出证明；2025比赛5/6题解出。
最近材料 2025-07-21 · 限定输入下由系统执行人：独立检查严密性、新颖性与适用条件
M05
搜索更好的数学/计算算法 ↘
● 限定评测系统搜索并验证候选算法；指定复矩阵乘法构造从49降到48次标量乘法。
最近材料 2025-05-14 · 限定输入下由系统执行人：设计目标/约束，证明并核对总成本
M06
检索文献并协作推进研究证明 ↘
◆ 研究案例研究Agent检索文献、起草和迭代论证；专家仍指导并核对研究。
最近材料 2026-02-11 · 人机协作人：选择问题、查原文、判断新颖性与最终发表
卡片标签表示最近公开材料的性质，不是这个任务整体已能自动完成；历史能力并不因后来的限制记录被删除。
看发展速度 · 看交接怎样变
从人工形式化到自然语言接题
两份材料相隔 361 天日历间隔，不是能力倍增时间
官方年度结果之间，输入与产物的交接方式明显改变；题目和研究配置也变了，因此只展示间隔与条件，不计算统一能力增长率。
怎样读这个时间轴
主轴按原始材料公开日期；实验/上线时点另列。历史空白仅表示本次未收录证据；后来的质疑不偷偷改写早期结果。
覆盖的含义：在指定输入、环境和验收下，材料支持AI参与哪些动作；未知比例保持null。
速度的含义：证据节点之间的日历间隔、流程交接变化；指标/样本/预算不一致时，不计算能力增长率或外推一年三年。
目的性选择三个领域的代表任务，不是穷尽检索或无偏职业采样；基础时间轴于2026-10-14核对，本次精选补充与证据截止2026-10-15，固定论文优先，不把动态榜排名倒填历史。
每个任务保留人的核验与决策；材料数量不等于独立实验数量，模型、Agent框架、重试预算和完整验收一并阅读。历史研究今天读取，不是当时保存的逐日网络档案。
逐项可查
任务、条件与原始证据
任务切片 M01
写出多步数值问题的推导
- 输入
- 文字应用题、数量与单位
- 交付
- 答案、步骤及可重算表达式
- 人继续负责
- 核对单位、条件与每一步理由
- 证据适配
- GSM8K是小学应用题的相近测试；不是专业数学工作覆盖率
任务验收：数字可重算；条件无遗漏；步骤与答案一致。
公开 2021-10-27 · 论文对照发现改进；本条未摘录数值通过率
多候选加验证器开始改善多步计算
GSM8K包含约8500道2–8步应用题；专门训练的验证器在多候选中选答案，比微调基线更有效。
工作含义：推导并非生成一次就可靠；候选与核对环节开始成为工作流。；依据：GSM8K：多步应用题与验证器
多候选加验证器开始改善多步计算
GSM8K包含约8500道2–8步应用题；专门训练的验证器在多候选中选答案，比微调基线更有效。
- 配置 / 输入
- GPT-3系列微调，生成多个候选并排序；计算器注释
- 衡量什么
- 论文对照发现改进；本条未摘录数值通过率
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 推导并非生成一次就可靠；候选与核对环节开始成为工作流。
- 比较条件
- 任务/配置或指标不同，不计算统一增长率
- 限制
- 验证器判断不等于数学证明；英语小学题不是专业工作样本。
公开 2023-03-15 · 指定测试最终答案准确率
通用模型在应用题上取得高分
GPT-4首稿在GSM8K报告92.0%最终答案正确。
工作含义：可以让模型起草推导，再独立重算数字与步骤。；依据：GPT-4技术报告首稿
通用模型在应用题上取得高分
GPT-4首稿在GSM8K报告92.0%最终答案正确。
- 配置 / 输入
- 5-shot思维链；预训练含部分GSM8K训练集
- 衡量什么
- 指定测试最终答案准确率
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 可以让模型起草推导，再独立重算数字与步骤。
- 比较条件
- 任务/配置或指标不同，不计算统一增长率
- 限制
- 训练与提示不同于2021验证器；分数不证明每个中间步骤可靠。
公开 2023-10-23 · 最终答案准确率，不是每条推导正确率
文字推导与程序计算分工
GSM8K测试1,318题；同一表2中Codex CoT 63.1%、PoT 71.6%，采用少样本贪心设置。
工作含义：数值答案可由执行器复算；题意到表达式的转换不因能运行而自动正确。；依据：Program of Thoughts：外部计算接口（v4）
文字推导与程序计算分工
GSM8K测试1,318题；同一表2中Codex CoT 63.1%、PoT 71.6%，采用少样本贪心设置。
- 配置 / 输入
- code-davinci-002；Python3.8/SymPy；同论文提示/执行系统比较
- 衡量什么
- 最终答案准确率，不是每条推导正确率
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 数值答案可由执行器复算；题意到表达式的转换不因能运行而自动正确。
- 比较条件
- 只解释这一来源/任务/配置；不与其他题集连成增长曲线
- 限制
- 小学多步题，不代表高难证明或自然语言推导全通过。
公开 2025-10-02 · 最终答案与裁判接受的推理过程是不同目标
答案命中与推理过程判定给出不同图景
Wen等在Qwen2.5-32B/DAPO-Qwen-32B的AIME24/25配置中观察：高K下答案覆盖可接近，但裁判接受的过程覆盖仍有差距；只保留定性图结论。
工作含义：选择验收对象会改变所谓能力边界；需要核对过程和裁判可靠性。；依据：RLVR推理过程核验研究（v2）
答案命中与推理过程判定给出不同图景
Wen等在Qwen2.5-32B/DAPO-Qwen-32B的AIME24/25配置中观察：高K下答案覆盖可接近，但裁判接受的过程覆盖仍有差距；只保留定性图结论。
- 配置 / 输入
- Qwen2.5-32B与DAPO-Qwen-32B；DeepSeek-R1-0528-Qwen3-8B裁判，每条推导裁判3次；any至少1次接受/all全部接受/majority多数接受；生成候选K最高1024
- 衡量什么
- 最终答案与裁判接受的推理过程是不同目标
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 选择验收对象会改变所谓能力边界；需要核对过程和裁判可靠性。
- 比较条件
- 只解释这一来源/任务/配置；不与其他题集连成增长曲线
- 限制
- 图值未数字化；依赖模型裁判，不能称Lean内核通过或无争议正确推理。
公开 2025-11-24 · Pass@K：K次中至少一次答案命中，不是单次或过程保证
多次尝试的答案覆盖不等于单次可靠
Yue等在特定模型/题集上比较不同采样K的答案覆盖；高预算下基础模型与RLVR模型的覆盖可能接近。
工作含义：记录全部尝试和选答案成本，不能只展示最终成功的一次。；依据：RLVR答案覆盖研究（v5）
多次尝试的答案覆盖不等于单次可靠
Yue等在特定模型/题集上比较不同采样K的答案覆盖；高预算下基础模型与RLVR模型的覆盖可能接近。
- 配置 / 输入
- Qwen2.5-7B-Base 与 SimpleRL-Qwen2.5-7B；AIME24 K=1024、MATH500 K=128；主实验T=0.6；仅选固定v5这一组作方法参考
- 衡量什么
- Pass@K：K次中至少一次答案命中，不是单次或过程保证
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 记录全部尝试和选答案成本，不能只展示最终成功的一次。
- 比较条件
- 只解释这一来源/任务/配置；不与其他题集连成增长曲线
- 限制
- 有限采样与不同题目/训练条件；不据此断言RL永远没有新能力。
任务切片 M02
构造并检查几何证明
- 输入
- 限定平面几何命题和图形关系
- 交付
- 证明或辅助构造
- 人继续负责
- 核对形式表达、图形假设与推广
- 证据适配
- 人工翻译到专用经典几何语言的任务，不含不可表达的几何不等式/组合几何；不能推广至任意数学领域。
任务验收：每步由允许规则推出；命题没有被削弱；图形退化条件处理。
公开 2024-01-17 · 25/30限定几何题；标准竞赛时间限制
专用系统找到非显然几何构造
AlphaGeometry在IMO-AG-30的30道平面几何题中解出25道。
工作含义：辅助构造搜索可以由系统承担，命题和推演范围仍需核对。；依据：AlphaGeometry发布；AlphaGeometry原始研究
专用系统找到非显然几何构造
AlphaGeometry在IMO-AG-30的30道平面几何题中解出25道。
- 配置 / 输入
- 2000–2022年IMO历史题；人工翻译成专用语言的经典平面几何命题，语言模型提出辅助构造、符号引擎推演。
- 衡量什么
- 25/30限定几何题；标准竞赛时间限制
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 辅助构造搜索可以由系统承担，命题和推演范围仍需核对。
- 比较条件
- 任务/配置或指标不同，不计算统一增长率
- 限制
- 表达法不含不能转换的几何不等式和组合几何；不是全部平面几何或25/30数学研究工作可委派。
任务切片 M03
为形式化命题搜索机器可检证明
- 输入
- 用逻辑语言写出的命题、库与环境版本。形式化是把问题及条件写成计算机可逐步核查的语言；Lean是这种证明检查工具。
- 交付
- 可由内核检查的证明文件
- 人继续负责
- 检查所写形式命题是否正是原问题，核对假设与自然语言含义
- 证据适配
- 形式化已提供命题的证明搜索；不等于自动选题及发表研究
任务验收：固定Lean环境重放通过；不额外假定结论，不用未完成证明占位；自然语言与形式命题一致。
公开 2024-07-25 · 组合系统的竞赛分；不是AlphaProof单独4/6
形式证明扩展到多种竞赛命题
AlphaProof完成2道代数与1道数论题；配合AlphaGeometry2，共4/6题、28/42分。
工作含义：系统可搜索机器可检证明，但自然语言与形式命题的转换仍由人承担。；依据：AlphaProof与AlphaGeometry 2：IMO2024
形式证明扩展到多种竞赛命题
AlphaProof完成2道代数与1道数论题；配合AlphaGeometry2，共4/6题、28/42分。
- 配置 / 输入
- 专家先形式化；AlphaProof使用Lean；系统部分题耗时最长3天
- 衡量什么
- 组合系统的竞赛分；不是AlphaProof单独4/6
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 系统可搜索机器可检证明，但自然语言与形式命题的转换仍由人承担。
- 比较条件
- 任务/配置或指标不同，不计算统一增长率
- 限制
- 不能拿组合成绩当Lean工具通用成功率。
公开 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首稿
开放证明模型可按预算测量
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年度得分直接连线。
任务切片 M04
起草自然语言的高难度证明
- 输入
- 竞赛级命题、时间与工具约束
- 交付
- 供专家评分的完整论证
- 人继续负责
- 独立检查严密性、新颖性与适用条件
- 证据适配
- IMO是严密推理的代理任务；不是职业数学家的任务分布
任务验收：完整证明而非最终答案；专家逐步核对；公开配置与所有尝试。
公开 2024-07-25 · 竞赛题结果，流程需翻译
证明稿仍依赖人工形式语言翻译
IMO2024组合系统4/6题、28/42分，先由专家翻译到形式语言，再得到证明。
工作含义：严密证明的局部搜索已有证据，自然语言交接还需要人补桥。；依据：AlphaProof与AlphaGeometry 2：IMO2024
证明稿仍依赖人工形式语言翻译
IMO2024组合系统4/6题、28/42分，先由专家翻译到形式语言，再得到证明。
- 配置 / 输入
- 研究专用系统；部分问题计算最长3天
- 衡量什么
- 竞赛题结果，流程需翻译
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 严密证明的局部搜索已有证据，自然语言交接还需要人补桥。
- 比较条件
- 任务/配置或指标不同，不计算统一增长率
- 限制
- 不同于普通聊天模型直接接题；与2025题目不同。
公开 2025-07-21 · 特定研究系统的比赛得分
自然语言接题并交付可评分证明
高级Gemini Deep Think研究版本用自然语言完成5/6题、35/42分，达到IMO2025金牌标准。
工作含义：约一年间，人工形式化交接扩展到直接自然语言输入与证明输出。；依据：Gemini Deep Think：IMO2025
自然语言接题并交付可评分证明
高级Gemini Deep Think研究版本用自然语言完成5/6题、35/42分，达到IMO2025金牌标准。
- 配置 / 输入
- 额外强化学习与并行思考；官方文述4.5小时时限；IMO协调者按学生标准评分
- 衡量什么
- 特定研究系统的比赛得分
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 约一年间，人工形式化交接扩展到直接自然语言输入与证明输出。
- 比较条件
- 任务/配置或指标不同，不计算统一增长率
- 限制
- 题目、系统与计算配置均变化；不是所有Gemini产品具备同样能力。
任务切片 M05
搜索更好的数学/计算算法
- 输入
- 目标问题、可执行评估器与预算
- 交付
- 候选算法及验证产物
- 人继续负责
- 设计目标/约束，证明并核对总成本
- 证据适配
- AlphaEvolve实例是复矩阵乘法搜索，非任意优化项目成功率
任务验收：在指定数域中正确；独立验证目标改进；不把算术次数当运行时收益。
公开 2025-05-14 · 同一指定算法问题的算术次数改善
候选算法搜索改善复矩阵乘法
AlphaEvolve发现4×4复矩阵乘法只用48次复数标量乘法，原已知Strassen构造49次。
工作含义：可以把候选方案探索交给搜索系统，人设计验证器并核对总成本。；依据：AlphaEvolve发布
候选算法搜索改善复矩阵乘法
AlphaEvolve发现4×4复矩阵乘法只用48次复数标量乘法，原已知Strassen构造49次。
- 配置 / 输入
- Gemini提出代码、自动验证与演化搜索；指定数域/目标
- 衡量什么
- 同一指定算法问题的算术次数改善
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- 可以把候选方案探索交给搜索系统，人设计验证器并核对总成本。
- 比较条件
- 同一指定复数问题的49→48可比；旧基线1969年，不等于AI年度增长速度
- 限制
- 不是实数标量48次；不保证任意硬件运行更快。
任务切片 M06
检索文献并协作推进研究证明
- 输入
- 研究命题、文献与专家反馈
- 交付
- 论证草稿、引用与待核对项
- 人继续负责
- 选择问题、查原文、判断新颖性与最终发表
- 证据适配
- 专家指导的研究过程案例；不是自主研究完成的受控测量
任务验收：引用确实支持命题；语义及逻辑独立核对；失败与人的修改全部保留。
公开 2026-02-11 · 研究过程/产物报告；本条无通用成功率
专家协作的研究Agent过程公开
Deep Think/Aletheia使用生成、核对、修订与原文搜索循环。一个具体协作例是独立集问题：研究哪些网络顶点能彼此不相邻地选出；Aletheia提出高层证明路线，研究者将它补成完整严密证明。
工作含义：AI参与文献与局部论证，数学家继续选题、核对引用和新颖性。；依据：Deep Think/Aletheia研究协作；Aletheia研究过程固定首稿
专家协作的研究Agent过程公开
Deep Think/Aletheia使用生成、核对、修订与原文搜索循环。一个具体协作例是独立集问题：研究哪些网络顶点能彼此不相邻地选出；Aletheia提出高层证明路线，研究者将它补成完整严密证明。
- 配置 / 输入
- 研究Agent、Google Search/web browsing、专家方向与反馈
- 衡量什么
- 研究过程/产物报告；本条无通用成功率
- 事件 / 运行
- 原文未给精确运行日期；上方为材料公开日
- 对任务意味着
- AI参与文献与局部论证，数学家继续选题、核对引用和新颖性。
- 比较条件
- 任务/配置或指标不同，不计算统一增长率
- 限制
- 本条选择人机协作切片；报告中的其它自主案例需另审。自然语言核对器不是Lean内核，不能据此得出任意研究题自主完成率；原文也提醒成功案例稀少、语义误解和引用错误。
本时间点的证明材料与综述
整理于 2026-10-19；各条实际阅读日另列。仅显示截至 2026-10-19 已公开的入选材料。综述用于发现任务，不作为独立通过率证据。
研究基准 · BM01 · BM01
GSM8K：多步应用题与验证器 ↗
公开日期 2021-10-27 · 页面标示发布日期或固定预印本v1页首日期
原文位置：§2数据；§4.2验证器；§4与附录C计算器
实际阅读 2026-10-14 · 英语小学应用题，计算器和多候选验证配置；不等于研究数学 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
发布方基准 · BM02 · BM02
GPT-4技术报告首稿 ↗
公开日期 2023-03-15 · 页面标示发布日期或固定预印本v1页首日期
原文位置：表2 GSM-8K；附录E训练集使用
实际阅读 2026-10-14 · 5-shot思维链，训练含部分GSM8K训练集；最终答案分不保证每步论证正确 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
发布方基准 · BM03 · alphageometry-study
AlphaGeometry发布 ↗
公开日期 2024-01-17 · 页面标示发布日期或固定预印本v1页首日期
原文位置：IMO-AG-30与symbolic deduction介绍
实际阅读 2026-10-14 · 2000–2022年30道平面几何题；专用符号系统，不能外推全部数学 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
竞赛结果 · BM04 · imo-deepmind
AlphaProof与AlphaGeometry 2：IMO2024 ↗
公开日期 2024-07-25 · 页面标示发布日期或固定预印本v1页首日期
原文位置：人工形式化说明；4/6题与28/42分
实际阅读 2026-10-14 · 4.5小时×两场是学生制度；系统耗时最长3天，不是同时间预算 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
竞赛结果 · BM05 · imo-deepmind
Gemini Deep Think：IMO2025 ↗
公开日期 2025-07-21 · 页面标示发布日期或固定预印本v1页首日期
原文位置：Breakthrough Performance；Making the most；IMO认证范围脚注
实际阅读 2026-10-14 · 特定高级研究版本；不同年度题目/配置；认证解答不等于审计整个运行 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
研究基准 · BM06 · BM06
DeepSeek-Prover-V2首稿 ↗
公开日期 2025-04-30 · 页面标示发布日期或固定预印本v1页首日期
原文位置：§3及§3.1 Experimental Results；表1（671B CoT/候选预算）、表2（题目类别）；附录C题集修订。
实际阅读 2026-10-14 · 671B CoT的88.9%为pass@8192；82.4%为pass@32，61.9%为pass@1；不是首试成功率 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
发布方研究 · BM07 · alphaevolve
AlphaEvolve发布 ↗
公开日期 2025-05-14 · 页面标示发布日期或固定预印本v1页首日期
原文位置：自动评估流程；Discovering new algorithms中的4×4复矩阵
实际阅读 2026-10-14 · 48次复数标量乘法不等于48次实数乘法或完整运行时加速 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
发布方研究 · BM08 · aletheia-research
Deep Think/Aletheia研究协作 ↗
公开日期 2026-02-11 · 页面标示发布日期或固定预印本v1页首日期
原文位置：The Frontier of Pure Mathematics；generator/verifier/reviser与expert collaboration
实际阅读 2026-10-14 · 发布方研究过程报告，专家指导；未复核全部研究产物，不提供通用证明成功率 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
综述 · BS02 · BS02
数学推理综述 ↗
公开日期 2025-06-10 · 页面标示发布日期或固定预印本v1页首日期
原文位置：§3推理组成；§4方法；§5–6局限
实际阅读 2026-10-14 · 综述用于任务框架与机制，不回填更早年份的已知成绩 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
综述 · BS03 · BS03
自动形式化综述 ↗
公开日期 2025-05-29 · 页面标示发布日期或固定预印本v1页首日期
原文位置：formalization定义；评测/语义对齐讨论
实际阅读 2026-10-14 · 机器核查形式命题不保证与自然语言原问题等价 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
同行评议研究 · BM09 · alphageometry-study
AlphaGeometry原始研究 ↗
公开日期 2024-01-17 · 页面/论文首稿标示公开日期
原文位置：Empirical evaluation：专用经典几何语言、人工翻译与不能表达的任务范围
实际阅读 2026-10-14 · 不含不可表达的几何不等式和组合几何；入口可能需浏览器接受cookie · 独立数学审阅直接核对Empirical evaluation；主Agent该入口遇到cookie重定向；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
研究预印本 · BM10 · aletheia-research
Aletheia研究过程固定首稿 ↗
公开日期 2026-02-10 · 页面/论文首稿标示公开日期
原文位置：§3.2人机协作/独立集问题；§4.2局限与语义误解；最终人的署名责任
实际阅读 2026-10-14 · 本页选取协作实例，不将文中其它自主案例或成功筛选集推广为通用研究成功率 · 本轮直接阅读所列原文位置；未复跑实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
数值任务研究预印本 · BF06 · program-of-thoughts
Program of Thoughts：外部计算接口（v4） ↗
公开日期 2023-10-23 · 固定v4页首：2023-10-23；不把v4表格倒填v1
原文位置：§2.2；§3.1数据/实现/指标；§3.2表2
实际阅读 2026-10-15 · 同底层模型改变提示与执行流程；未匹配完整延迟/预算；不是端到端财务工作通过率 · 本轮直接核对所列原文位置/版本；未复跑外部实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
推理评测研究预印本 · BM11 · rlvr-answer-support
RLVR答案覆盖研究（v5） ↗
公开日期 2025-11-24 · 固定v5：2025-11-24；具体结论以所引用版本为准
原文位置：§3设置；表2；附录C.7覆盖与C.8温度分析
实际阅读 2026-10-15 · 有限采样只测答案命中；特定模型/任务结果不等于所有推理机制；不与另一论文合并效应 · 本轮直接核对所列原文位置/版本；未复跑外部实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
推理评测研究预印本 · BM12 · rlvr-judged-traces
RLVR推理过程核验研究（v2） ↗
公开日期 2025-10-02 · 固定v2页首：2025-10-02；不倒填首次预印本日期
原文位置：§3.1图2；§3.2图3；附录A.3裁判方法
实际阅读 2026-10-15 · 推理过程由模型裁判判定，有any/all/majority规则；不是形式证明内核，图值未可靠转录则定性 · 本轮直接核对所列原文位置/版本；未复跑外部实验
当前引用状态：可引用；不等于现场验证。状态取自整理于 2026-10-19 的当前模块，不表示历史视角当时已知。
网站维护记录
编辑历史
这些是网站记录的修订
工作建议变化和资料维护分开记录。没有可比运行时，不把页面更新称为AI能力进步。
工作建议变化新增工作流
OSWorld 2.0补充长流程与跨应用证据
对工作的影响
系统交接增加跨应用状态核对、部分失败与恢复检查；这是方法建议，不是现场成功率提升。
原依据 / 条件
主要参考单应用或较短操作任务
新依据 / 条件
新增108个长流程任务与整题/部分评分
企业交付页加入状态恢复、跨来源核对和最终验收要求，仍不宣称现场采用已验证。
查看原始依据与限制 →工作建议变化新增方法
失败诊断也有可引用的评测
对工作的影响
Agent失败后保留轨迹与根因判断，分别验收诊断是否正确、修复是否有效。
原依据 / 条件
仅从是否完成观察Agent表现
新依据 / 条件
引入失败定位与根因分类证据
DEV-04增加失败轨迹审查；诊断增益与修复完成度分开展示。
查看原始依据与限制 →