数学 × AI 周报 · 第 04 期：陶哲轩把旧代码交给 AI，把证明留给自己
第 04 期：陶哲轩让 AI 编程智能体把自己 1999 年写的 Java 小程序搬到网页，顺手挑出两个他没发现的 bug，并亲口划出"视觉辅助"与"数学论证核心"的边界；第三届 AI for Math 工作坊在首尔 ICML 举行，投稿量较去年翻倍；IMO 2026 上海本周开幕，7 月 15—16 日笔试，AI 阵营的表态成为悬念。
本期一句话：这周没有人宣布”AI 证明了什么”，陶哲轩却用一次亲身示范，把”哪些活该交给算，哪些活必须自己证”这条线画得清清楚楚。
陶哲轩：AI 编程智能体帮我把 27 年前的小程序搬上网页，还顺手挑出两个我没发现的 bug
7 月 11 日，陶哲轩在博客发文《Old and new apps, via modern coding agents》，回顾了自己从 1999 年起就在做”机器辅助数学”这件事——当年他用 Java 1.0 写了一批复分析、线性代数和数学可视化小程序（其中”蜂巢”小程序与 Allen Knutson 合写），大约二十多个。这些 Java Applet 在 2008 年前后随浏览器标准变化陆续失效，此后一直搁置。
这一周，他让一个现代 AI 编程智能体把这批旧程序整体迁移成 JavaScript，几个小时内就完成了原本需要大量人工的搬迁工作，并新做了一个狭义相对论时空图工具和一个 Gilbreath 猜想可视化。过程中，智能体发现了两处他自己都不知道的旧代码 bug；他本人复核时又额外挑出一处拖拽事件处理的小毛病。他写道：”因为这些小程序只是辅助性的可视化工具，而不是数学论证中的关键环节，这类 bug 带来的下行风险相对较低。”
7 月 12 日，他又发了一篇《A random variable visualizer》，把自己 2016 年因为太费时间而搁置的一个想法——把随机变量做成动画可视化——用 AI 编程智能体在几轮来回后做出了一个可用的原型：一个简化版”Python + Excel”式的小型语言，可以定义随机变量、做算术运算或条件化，再生成动画或文字输出。
解读：这两篇博客本身就是”算”与”证”边界的最佳注脚。陶哲轩没有用 AI 去动他真正的数学论证——他把 AI 用在了”辅助可视化”这类容错率高的环节，还专门说明了”下行风险相对较低”这个判断标准。这恰恰是普通数学工作者可以直接抄的作业：AI 编程能力已经强到能几小时内复活 27 年的遗留代码，但”哪块地方允许出错、哪块地方绝对不允许”，仍然需要数学家自己来划线。
来源：陶哲轩博客 · Old and new apps · 陶哲轩博客 · A random variable visualizer
第三届 AI for Math 工作坊在首尔举行：投稿量翻倍，五大方向全部指向”可核验”
7 月 11 日，第三届 AI for Math 工作坊在 ICML 2026 期间于韩国首尔 COEX 会展中心举行。据工作坊官网披露，本届收到 346 篇投稿，是去年的两倍。
工作坊设定的五大核心方向分别是：超越竞赛题难度的形式定理证明、连接形式与非形式数学的精确自动形式化、自然语言数学推理管线、跨学科科学问题求解应用，以及引入视觉信息的多模态推理。受邀报告嘉宾包括 Project Numina 的 Jia Li、AWS/Lean FRO 的 Leonardo de Moura、Rutgers 大学的 Emily First、字节跳动 Seed 团队的 Zheng Yuan 等。往届最佳论文得主分别是 2025 年的《Limit of RLVR》与 2024 年的 PutnamBench，本届最佳论文奖金为 1,500 美元。
解读：投稿量翻倍是一个粗糙但直观的信号——”AI 做数学”已经从几个实验室的孤例，变成了一个有稳定投稿池、有连续三届历史的研究方向。更值得注意的是五大方向的措辞：不是”解出更多题”，而是”形式定理证明”“精确自动形式化”这类围绕可核验性搭基础设施的表述。赛道在变宽，但赛道两侧的护栏（验证、形式化）也在同步变密。
IMO 2026 上海开幕：笔试将至，AI 阵营的表态仍是悬念
第 67 届国际数学奥林匹克（IMO 2026）于7 月 10 日起在上海举行，各代表队领队本周抵达，官方日程为 7 月 14 日开幕式、7 月 15—16 日两场笔试、7 月 20 日闭幕式。
截至本期发稿，尚未检索到任何 AI 实验室就 2026 年参赛/评分政策发布官方声明。回顾去年（2025 年，澳大利亚）：闭幕式结束后，OpenAI 自行宣布模型达到”金牌”分数线，但未经 IMO 官方评分员核验；DeepMind 则选择等待官方认证再公布结果。这场争议在本报第 01、02 期已有详述，也是本报持续追踪的一条主线。
解读：这周还没有真正的头条——头条要等到 7 月 15、16 日笔试结束之后。但悬念已经摆在桌面上：今年会不会有实验室愿意让官方评审员核验分数，而不是像去年那样自行宣布？前两条新闻描述的”可核验”氛围（陶哲轩自己划线、AI for Math 工作坊全面转向形式化）会不会真的传导到这场最有公众曝光度的测试里，下期见分晓。
把这一周连起来看
这三条新闻共享一条主线：这周没有新的”AI 破解了什么”头条，但”算”与”证”之间那条线，被从三个不同角度描得更清楚了。
陶哲轩用自己的工作流做了示范——AI 编程智能体值得信赖到可以放手处理”辅助可视化”，但”论证核心”仍然自己把关，他甚至明确写出了判断标准。AI for Math 工作坊的投稿翻倍说明”用 AI 做数学”这件事本身在快速扩张，但工作坊设定的五个方向几乎都在谈形式化和可核验，而不是单纯的解题能力。IMO 2026 上海本周开幕，真正的考验在笔试之后——去年”自己宣布金牌”和”等官方认证”的分野，会不会在这一年重演，是留给下周的悬念。
机器能干的活越来越多，但谁来把关”这一步真的对不对”，仍然是数学家自己的事。这正是”证”越来越值钱的原因。
机器越来越会算，「证」也就越来越值钱。
—— 数学 × AI 周报 · 第 04 期。