数学 × AI 周报 · 第 05 期：一周两个「证明」头条，一个签字画押，一个悬而未决
第 05 期：OpenAI 称 GPT-5.6 Sol Ultra 用 64 个子智能体一小时内"证明"了悬而未决 50 年的循环双覆盖猜想，十天过去仍无人正式核验；宾大统计学者 Edgar Dobriban 用 GPT-5.6 Sol Pro 90 分钟推翻 Benjamini-Hochberg 方法 30 年来的一个假设，并亲自核验、给出机器可验证证书；IMO 2026 上海笔试结束，AI 阵营的官方表态仍是悬念；中国科学院数学与系统科学研究院发布数学研究智能体 MMAT，攻克 8 个长期公开问题。
本期一句话：这周有两条”AI 证明了几十年老猜想”的头条前后脚出现——一条挂在公司服务器上十天，至今没人签字确认；另一条被作者本人亲手核验、附上机器可查的证书。同一种句式的头条，含金量能差出一个数量级。
OpenAI 称 GPT-5.6 Sol Ultra”证明”了 50 年悬而未决的循环双覆盖猜想，十天过去仍悬着
7 月 10 日，OpenAI 宣布其模型 GPT-5.6 Sol Ultra 在不到一小时内生成了循环双覆盖猜想（Cycle Double Cover Conjecture）的完整证明。这一猜想由 George Szekeres（1973 年）与 Paul Seymour（1979 年）分别独立提出，问的是：任意无桥图，是否都存在一组回路，让每条边恰好被覆盖两次？它是图论中悬置时间最长的公开问题之一。
据 OpenAI 公布的材料，系统调用了 64 个动态管理的子智能体并行探索不同证明路径——代数视角、结构归纳等——早期阶段刻意维持路径多样性，遇阻的智能体会被标记、只在出现新思路时才重新介入，另设”对抗型”智能体专门找漏洞。证明全文与所用提示词都以 PDF 形式发布在 OpenAI 自己的服务器上，写作环节由 Codex 协助整理，但 OpenAI 强调数学内容完全出自 GPT-5.6 Sol Ultra。
反应两极：普林斯顿数学家 Noga Alon 称这个猜想”广为人知”，证明的简洁程度出乎意料；曼彻斯特大学的 Thomas Bloom 评价”是个很不错的证明”，”简短、初等，放在 1980 年代都可能被发现”，但也指出证明完全没有引用前人工作——一篇 1983 年的基础论文只字未提。截至本文发稿（7 月 20 日），距离首次公布已过去十天，学界仍未完成正式核验。这个猜想过去也曾多次出现”证明”，其中不止一篇发在 arXiv 上，后来被发现有漏洞或主动撤回。
解读：把证明 PDF 发在公司 CDN 上，和把证明发表在经过同行评议的期刊上，是两件不同的事——这周几乎所有严肃报道都在反复强调这一点。”看起来像证明”和”就是证明”之间的落差，短期内会一直是 AI 数学最真实的生存状态。下一条新闻恰好提供了一个对照组。
宾大统计学者亲自核验：GPT-5.6 推翻统计学 30 年猜想，附机器可验证证书
7 月 14 日，宾夕法尼亚大学统计学者 Edgar Dobriban 用 GPT-5.6 Sol Pro 构造出一个反例，推翻了围绕 Benjamini-Hochberg（BH）方法的一个 30 年猜想。BH 方法由 Yoav Benjamini 与 Yosef Hochberg 于 1995 年提出，用于控制多重假设检验中的错误发现率（FDR），是统计学中被引用超过 13 万次的基石级方法。学界此前普遍相信，面对相关的双侧高斯检验统计量，BH 方法依然能把错误发现率控制在目标水平之内——这个假设一直没有被严格证明，也没有被推翻，直到这周。
Dobriban 构造了一个具体的因子模型：在显著性水平 α = 0.01 下，一份基于区间算术的严格证书证明，当假设检验数量足够大时，实际错误发现率会超过 0.0104——差距不大，但确实存在，说明这个 30 年来被广泛默认的假设是错的。此前 GPT-5.5 在同一个问题上耗时约 20 小时未果，GPT-5.6 Sol Pro 只用了约 90 分钟。Dobriban 本人逐步核对了整个证明，并把完整对话记录、代码和论文全部公开发布在 arXiv 上。加州大学伯克利分校统计学者 Will Fithian 评价：”这是我所在统计学领域里最有意思的公开问题——换作是哪位统计学家亲手构造出这个反例，我都会由衷替他们高兴。GPT-5.6 解决了它，但我还是希望是个人做到的。”
解读：这才是”证”该有的样子——不是一份挂在服务器上等人围观的 PDF，而是一位有名有姓的研究者亲自核验、公开全部推理过程、诚实标注影响幅度还有待评估。和上一条新闻放在一起看，两条头条用的都是”AI 推翻/证明了 XX 年老问题”这句话，但一条十天没人签字，一条几天内就有人签了字——这周的新闻恰好把”算”和”证”的分野摆在了同一张桌子上对比。
IMO 2026 上海笔试结束，AI 阵营的表态仍是悬念
第 67 届国际数学奥林匹克（IMO 2026）7 月 15—16 日在上海完成两场笔试，每场 4.5 小时、三道题，满分 42 分。评注博主 Evan Chen 已于 7 月 18 日发布本届题目的解题笔记。截至本文发稿（7 月 20 日，闭幕式前），官方尚未公布成绩，OpenAI、DeepMind 等实验室也都还没有就本届赛题发表任何战绩声明。
对照去年（2025 年）：OpenAI 在赛事结束后不久自行宣布模型拿到”金牌”分数（35/42），未经官方评审员核验；DeepMind 的 Gemini Deep Think 则等待 IMO 官方评分员完成核验后才公布结果，并获得 IMO 主席 Gregor Dolinar 的正面评价。这场关于”自己宣布”与”官方核验”的分歧，本报第 01、02、04 期已连续追踪。今年，多个预测市场对”AI 拿到满分 42/42”给出了 85%～96% 的高赔率，但这些都只是交易者的赌注，不是任何形式的官方或学术验证。
解读：笔试结束了，真正的悬念才刚刚开始——今年会不会有实验室愿意让官方评审员核验分数，而不是像去年那样自己先宣布？这和本期前两条新闻问的其实是同一个问题：谁来确认这个结果为真，以及愿不愿意让别人来确认。
中国科学院发布数学研究智能体 MMAT：攻克 8 个长期公开问题
7 月 6 日，中国科学院数学与系统科学研究院发布基于大语言模型的数学研究智能体”数学机械化智能体”（MMAT）。据研究院介绍，MMAT 采用分层多智能体协同架构，由 20 个具备专项能力的子智能体组成，目标是覆盖数学研究从提出猜想到完成证明的全流程。
经过两个月的内部测试，MMAT 独立或与数学家交互，攻克了代数计算理论、微分代数、数论三个方向共 8 个长期公开问题：其中 2 个由 MMAT 全自动独立解决，另外 6 个由 MMAT 完成核心关键引理的证明，再由数学家完成余下工作。中国科学院院士、数学院院长张平表示，MMAT 的意义不止于单项技术突破，更有望推动数学研究范式发生深层次变革。
解读：与前面两条”模型单独产出一份证明，再等外界围观核验”的模式不同，MMAT 从设计上就把”人机交互”嵌进了研究流程——8 个问题里有 6 个是”AI 证明关键引理、人证明剩余部分”，核验环节内建在协作过程里，而不是事后补上。这与陶哲轩在本报第 01 期提出的”人类直觉 + 大语言模型生成 + 形式验证系统”三层协同构想相呼应。
来源：新浪财经报道
把这一周连起来看
这四条新闻共享一根主线：这周”AI 证明了什么”的头条格外密集，但含金量高度分化——分化的关键变量，是有没有人愿意把名字签在核验结果上面。
循环双覆盖猜想的证明发布十天，依然停留在”公司服务器上的一份 PDF”这一步；Benjamini-Hochberg 反例发布不到一周，已经有具名研究者亲自核验、公开全部推理过程和机器可查证书。同一周、同一种句式的头条，一个签了字，一个还悬着。IMO 2026 笔试刚刚结束，历史又一次把同样的问题摆到桌面：AI 阵营这次会不会愿意接受官方评审的核验，还是重复去年”自己先宣布”的剧本？中国科学院的 MMAT 则提供了第三种范式——把人机核验直接嵌进协作流程，而不是把证明扔出来之后才等外界围观。
机器能算出结果的速度还在指数级往上走，但”谁来确认这个结果是真的”这件事的成本，并没有跟着一起降下来。这正是”证”越来越值钱的原因。
机器越来越会算，「证」也就越来越值钱。
—— 数学 × AI 周报 · 第 05 期。