数学 × AI 周报 · 第 03 期：从「答对了」到「证明可查」

本期一句话：这周没有新的「AI 破解猜想」头条，社区在忙一件更慢的事——把上个月的结果拆开，看看每一步能不能被查。

---

陶哲轩逐行拆解：OpenAI 的构造到底强在哪

7 月 3 日，陶哲轩在个人博客发表长文，系统比较了三种攻克 Erdős 单位距离问题的构造，把它们放在同一条谱系上比较：

• 经典 Erdős 构造：单位距离对数下界约为 n^(1 + c/log log n)，其中 c 趋近于 log 2；
• “Mythos” 中间构造：由 AI 辅助分析发现，下界提升到 n^(1 + c/log log log n)；
• OpenAI 模型构造（最强）：直接给出 n^(1+c)（c 为某个正常数），目前已知 0.03583 ≤ c ≤ 1/3。

三者的技术差异在于如何在数域的代数整数环中构造满足 w·w̄ = m 的元素：经典构造固定扩张次数 D、只增加所用素数个数 t；Mythos 让 D 和 t 同步增长；而 OpenAI 的构造使用 Golod–Shafarevich 塔，让 D 可以无界增长，同时保持 t 不变——这是 δ 从”随 n 趋于 0”变成”严格为正”的关键一步。陶哲轩写道，这个结果的出现”多少有些意外”（it came as some surprise）。

解读：上个月大家关心的是”AI 是否推翻了猜想”，这周陶哲轩做的是数学家真正在做的事——不满足于”验证过是对的”，而要追问”为什么对、这一步和那一步的本质区别是什么”。这篇长文本身就是”证”与”算”区别的示范：算出答案只需要一次运行，讲清楚构造的谱系需要一位顶尖数学家坐下来写一整篇技术笔记。

来源：陶哲轩博客原文

---

“拉马努金 AI 挑战赛”上线：不比答案，比可核查的推导

7 月 2 日，Gil Kalai 在博客上公布了由 Ido Kaminer 牵头、依托 Ramanujan Machine 项目发起的”拉马努金 AI 挑战赛”，即日起至 8 月 1 日接受提交。

挑战包含 10 道研究级问题，都要求给出数学常数显式公式的严格推导——这与早期 Ramanujan Machine “让 AI 猜公式”的玩法不同，这次要的是从公式到证明的完整链路。提交形式可以是形式化证明（Lean 风格）、计算机代数系统（CAS）推导，或附带可复现代码的人类可读证明。Kaminer 的原话是：”目标不仅是测试 AI 能否找到答案，还要测试它能否产出一种可以被结构化核验的推导过程。”

解读：把这道题放在莱顿宣言（第 02 期）划出的边界上看，会更清楚它的意义——宣言呼吁的”AI 参与度公开、结果可核验”，这个挑战赛几乎是照单实现：不看你答没答对，看你能不能把过程摆到台面上让人查。这是社区自己动手把原则变成可执行的评测机制。

来源：Gil Kalai 博客原文

---

Lean 牵手 LMFDB：数论数据库开始为 AI 时代做准备

6 月 29 日至 7 月 3 日，”Bridging Lean and the LMFDB”工作坊在英国东英吉利大学召开，是”通过数学数据库实现可扩展定理证明”项目的第一场工作坊（第二场计划在 2027 年初于 MIT 举行）。项目由 AI for Math Fund 资助，管理方为 Renaissance Philanthropy，创始捐助方为 XTX Markets。

工作坊内容围绕 Lean 的数论接口（数域、椭圆曲线、模形式）与 LMFDB（L-函数与模形式数据库）的对接展开，其中三场报告直接指向 AI：David Roe 介绍 LMFDB 如何为大语言模型和形式化做适配；Paul Lezeau 讲如何用 AI 工具辅助形式化；Xindi Yang 展示了一套流程——纯 LLM 从论文生成 Lean 定义与命题陈述，再由人工精修，并用自动证明器补全证明中的空隙。

解读：这是一条容易被忽略但很重要的支线——AI 参与数学不只是”solve a hard problem”这种高光时刻，更多是这类基础设施建设：把数据库、证明助手和语言模型的接口一点点打通。资金已经从个别项目变成了专项基金，说明这件事正在从”极客尝试”变成”基础设施建设”。

来源：工作坊官网

---

费马大定理形式化工作坊在伦敦开幕：故意挑硬骨头考 AI

7 月 6 日至 10 日（今天开幕），Kevin Buzzard 在伦敦帝国理工学院主持的费马大定理（FLT）Lean 形式化工作坊启动，目标是把基于 Khare–Wintenberger/Kisin 路线（而非原始 Wiles/Taylor–Wiles 证明）的”21 世纪版”FLT 证明形式化到 Lean 中。

值得关注的是资助方之一 Logos Research——一家帝国理工孵化的初创公司，专做 AI 可靠性推理工具，顾问包括 Buzzard 本人和菲尔兹奖得主 Martin Hairer。他们提出用 AI 尝试自动形式化部分前置引理甚至部分主证明。Buzzard 的表态很谨慎：”虽然自动形式化最近进步不小，但它似乎仍不能可靠地自主完成定义的形式化，或以符合 Lean 风格的方式陈述定理。”组织者特意不去挑一个对 AI 友好的题目，而是直接选了 FLT 这样公认的硬骨头，以此判断自动形式化到底在哪里会失效。

解读：这场工作坊的价值恰恰在于它”故意不讨巧”。大多数自动形式化的展示案例都经过筛选，专挑 AI 擅长的部分秀成绩；Buzzard 团队反其道而行——先选最难的目标，再看 AI 能扛住哪一段、垮在哪一段。这种”压力测试”式的诚实,比一个漂亮的 demo 更有参考价值。

来源：Xena 博客原文 · Lean 官网 FLT 项目页 · 帝国理工新闻稿

---

IMO 2026 上海：本周开幕在即

第 67 届国际数学奥林匹克（IMO 2026）将于上海举行，官方日程为：7 月 10 日各代表队领队抵达，7 月 14 日开幕式，7 月 15—16 日两场笔试，7 月 20 日闭幕式。这是中国自 1990 年以来第二次承办 IMO，也是 IMO 历史上首次在一所高中校园（上海中学）举行。

去年（2025 年，澳大利亚）赛后，OpenAI 在闭幕式结束后立即自行宣布模型达到”金牌”分数线，未经 IMO 官方评分员核验；DeepMind 则选择等待官方认证。这场争议在本报第 01、02 期已有详述。截至发稿，尚未检索到 AI 实验室对 2026 年参赛/评分政策的官方表态。

解读：去年的教训很明确——”金牌”这个词的分量,取决于是谁在打分、有没有官方参与。今年 IMO 就在眼前，真正值得盯的不是”AI 又考了多少分”,而是这次会不会有实验室愿意让官方评审员来核验分数,而不是自己宣布自己拿了金牌。

来源：IMO 2026 官方日程 · IMO 官方页面

---

把这一周连起来看

这五条新闻有一条共同的主线：这周没有新的”AI 破解了什么”式头条,社区在忙的是更慢、更硬核的验收工作。

陶哲轩没有宣布新战果,而是坐下来把上个月的构造拆成三级台阶,讲清楚每一级”强”在哪里。拉马努金挑战赛把莱顿宣言的原则变成了具体的评测标准——不比答案,比推导能不能被核查。Lean 与 LMFDB 的对接工作坊,是把”AI 参与数学”从个别炫技案例变成长期资助的基础设施项目。Buzzard 的费马大定理工作坊则反其道而行,故意挑一块硬骨头,诚实地看自动形式化在哪里会垮。IMO 2026 上海一周后开幕,会不会重演去年”自己宣布金牌”的争议,是留给下周的悬念。

机器算得越来越快，但这周所有真正的进展,都发生在”算完之后”——拆解、核查、搭基础设施、故意找茬。这些工作不产生头条,但决定了下一次头条能不能站得住。

---

机器越来越会算，「证」也就越来越值钱。
—— 数学 × AI 周报 · 第 03 期。