跳转至

OpenAI 的两位数学家谈 Astra 的数学结果：球填充、非 sofic 群，以及"AI 的证明为什么都很短"（a16z，2026-09-08）

⚠️ 说话人认定：本页在两位嘉宾之间基本不做区分。 转录稿是自动字幕，只有 >>，没有姓名标签，而两位嘉宾是长期合作者（[00:02:01] 他们说此前合写过一篇论文），语流高度交错、互相接话补完。本页凡嘉宾观点一律写"两位数学家"或"OpenAI 一方"，只在下述极少数有明确锚点处分人： - [00:02:01]："我比 Matab 早一点加入……我去年夏天看到 IMO 金牌"——先加入的那位是 Mark；秋天 Mark 给了 Matab 一个 GPT-5 账号，Matab 由此"转化"。 - [00:03:02]："我specifically做组合数学"并讲 Erdős 问题站那段经历的，是 Matab（他随后说"我告诉了 Mark"）。

主持方的话本页写"主持人"。 ⚠️ 本期主持人发言占比很高且多为长段落的自我推演，引用时请注意区分哪些是 OpenAI 一方的表述。

专名对照表（转录稿拼写 → 本页采用）：Astro → Astra（OpenAI 模型）、GPD5/GPG5/GP5 → GPT-5、Erdish → Erdős、combinotaurics/cominatorial → combinatorics / 组合、Ruden → Rudin（《数学分析原理》）、Hails → Hales、VZOs/Viazosa → Viazovska、Conan Elkis → Cohn–Elkies、fouryear transform/foyer transform/for transform → Fourier transform（傅里叶变换）、leech lattice → Leech lattice、capski → （与前文的两位 1970 年代俄国数学家连读，疑为 Kabatiansky–Levenshtein，本库不认定）、lises/lettuce/lattise → lattice（格）、sophetic/sofic/non-sulfic/non-sitic/Sophie group → sofic / non-sofic group、subjunctive → surjunctive、gotch → Gottschalk、Aldos and Lyons/eldest Leon/all this lions → Aldous–Lyons（猜想）、unodularity/modularity → unimodularity、hilly graph → （整数的标准图表示，转录不清，本库不认定具体术语）、kay graph/kaly graph → Cayley graph、Andrew Wilds → Andrew Wiles、riskreward → risk–reward。

⚠️ 以下明确不裁决，照录存疑： - 两位嘉宾的姓名：转录稿写作 Mark Selki 与 Matab Swani（另出现 Matab）。疑为 Mark Sellke 与 Mehtaab Sawhney，但本库不作确证，见 人物页 的同样标注。 - EU um was actually your adviser（[00:01:01]）：主持人说的两人之间的学术关系，姓名转录不可辨，本库不猜。 - ⚠️ 球填充那个新界的具体数值形式（[00:23:18]）：转录为 "e to the 2 pi plus little o1 to the d"，约等于 "2 的 −0.61…d 次方"，主持人当场说"我以为是 604"。这个式子在转录稿里明显残缺且两人自己都在现场核对数字，本库只记录"它是一个漂亮的闭式、数量级约 2^(−0.6d)"，不照抄这个式子，也不替他们补全。 需要精确表述请查 OpenAI 的原始发布。 - Kun and Tom（[00:52:50]、[00:56:53]）：被 Astra 的证明引用、且已做出后续工作的两位数学家，姓名转录不完整，本库不认定。

概要

这是本库第一份来自前沿实验室内部、专门谈 AI 做数学的材料。此前本库关于 AI for Science 的材料要么来自应用侧的 neo-lab（Lila Sciences、Xaira、Genesis Molecular AI），要么来自实验室领导层的转述（Greg Brockman 提到的 Navier–Stokes）。这一期是实际把问题喂给模型、读它的思维链、再判断结果好不好的那两个人。

最该被单独引用的八条：

  1. ⚠️ "AI 的证明普遍很短、很优雅"——而且他们自己说这与预期相反（[00:53:51]–[00:55:52]）："一年前我会非常惊讶地得知这些 AI 证明都很短、很优雅。你原本担心它会生成一堆千页的东西、你永远看不懂——但结果恰好相反。" 配套的那句更尖锐："目前只有人类能产出 200 页的证明。"
  2. ⚠️ 他们给"AI 擅长什么"的两条相对优势非常具体（[00:05:03]）：① 对文献的熟悉——知道某个结果是否已经存在；② 一旦有了想法，把细节执行对——"每当你有一个想法，总要把一堆东西对齐（epsilon 是不是小于 delta 这类），人很容易在这些细节里迷失，而 AI 总是把这类论证钉死"。
  3. ⚠️ "可达结果的文艺复兴"这个说法的机制说得很清楚（[00:06:03]–[00:07:04]）：数学家的常态是试几小时、几天、几周然后放弃，因为风险回报不划算；而一两年后发现别人把你以为不成的那个想法做成了，是一种并不罕见的经历。他们的结论是——"把一个想法做成，本身就可能是战役的一大部分。" 而模型的姿态是"人让我做这个，那就做"。
  4. ⚠️ "上下文被污染"是他们给的人类劣势的核心隐喻（[00:09:05]）：人沿着一条错路走了一阵之后很难让大脑重新布线——最初的想法在脑子里已经和那些没走通的东西连在一起了，"你的 context window 有点被污染了，而你没法从上周的自己再克隆一份出来，说'别做这个，试别的方向'"。对 AI 这件事很容易。
  5. ⚠️ 球填充的结果是一个"等式"，不只是更好的界（[00:26:20]–[00:28:20]）：模型不仅构造出一个给出新界的函数 f，还证明了不存在更好的 f——"所以这是一个等式，相当强"。而给模型的指令基本上就是"分析这个高维线性规划，玩得开心"。
  6. ⚠️ 十个问题里只有一对是交互式的，而那次交互只是"你能再往前推一点吗"（[00:34:28]–[00:36:29]）：其余问题都是喂进去、模型交回解。那一次追问之后模型给出了复杂得多的表示论，并顺带导出了全空间球填充的猜想值。他们对"为什么第一次没推到底"的解释不是能力问题——"模型相当任务导向。你让它做一个任务，它完成了，它就挺满意的"、"它当时就是不想费那个劲"。
  7. ⚠️ 非 sofic 群的对照，本库认为是本期最强的一组量化对比（[00:51:50]–[00:52:50]）：更强的 Aldous–Lyons 猜想两年前被证伪，用的是约 250 页、建立在另外 200 页之上、动用量子复杂性理论的工作，"没有多少人能看懂"；而 Astra 直接证明存在非 sofic 群的那个证明大约 15 页，完全待在群论里。
  8. ⚠️ OpenAI 一方明确说他们训练的是通用推理模型，回溯与重开"不是数学特有的"（[00:13:07]）："这些是推理的通用工具，如果你在推理上下足功夫，最终就该看到这些模式。" ⚠️ 主持人特别指出这条路线不依赖自动形式化（autoformalization / Lean）来引导推理（[00:13:07]）——本库把这条记为 OpenAI 路线与形式化验证路线的分野。

核心观点

一、两个人是怎么被"转化"的

  • 第一位（[00:02:01]）：去年夏天看到 IMO 金牌，觉得"这太惊人了，我想看看他们到底干了什么"，于是去了 OpenAI。
  • 第二位（[00:02:01]–[00:03:02]）：秋天拿到一个 GPT-5 账号后开始玩模型，很快确信这非常令人兴奋。他的具体触发点值得单记：
  • 他做组合数学，而 Erdős 提出的一大批问题被收集在一个网站上。他的长期挫折是——看到一个标着 open 的问题，却不知道它是不是真的还没被解决，因为文献往往很难搜。
  • 他把一个这样的问题丢进 GPT-5，五分钟后它找到了文献。而这正是他和几个朋友已经花了几小时、还搞不清问题是否在能力范围之内的那个问题。"被告知'是的，这在能力范围内，这是做法'，那种感觉非常好。"
  • 他告诉了第一位，然后他们又找到了十来个类似的案例。
  • ⚠️ 他们强调这条"文献搜索"的优势到今天仍然成立（[00:05:03]）："对一切都熟悉这一点，肯定仍然是一个相对强项"，并且这会反过来影响 AI 正在解决的那类问题的类型。

二、AI 做数学的相对强项与弱项

  • 强项一：细节执行（[00:05:03]）：见概要第 2 条。
  • 强项二：敢于下不划算的注（[00:06:03]–[00:08:05]）：
  • 人的处境是"你是在跟问题赌博"——"也许我该试这个路子，但看起来不太可能成，不值得我花时间"。
  • 单位距离猜想（unit distance conjecture）那个例子：最终的构造可以被讲得跟人们以前试过的很像，但里面有大量极其琐碎挑剔的细节；模型靠把它已知的东西组合起来、加上不错的品味，下对了注。
  • ⚠️ 他们特别指出这个问题很多人想过："想法本身并不陌生，这大概说明很多人试过，或者至少有几位非常认真的数学家试过——这正是让它特别有意思的地方。"
  • 从思维链里能看到什么（[00:08:05]）：他们说在公开的摘要版思维链里可以看到它在像数学家一样推理——因为它知道几个非常正确的小事实，所以做出正确决策，最终能够剪枝。"它并不是在试所有东西。它试了很多不同的东西，它极其执着，但它不可能试每一个想法。"
  • 弱项对照：人为什么卡住（[00:09:05]，见概要第 4 条）。
  • ⚠️ 模型在"更新一条路径的成功概率"上比人更好（[00:10:06]）：他们说人在某个方法第一次不成时，会自动下调它成功的可能性，并且反复如此；而模型在好几个解法里看起来更善于更新这个概率——无论是拒绝一条路径，还是继续。
  • 但他们自己立刻给了一个更弱的解释（[00:10:06]）："即便不是这样，光是'你可以重开一个 model session'这件事就意味着……"——也就是说，至少一部分优势来自可以并行跑多个 agent，而不是来自更好的判断本身。⚠️ 本库认为这处自我限定很重要，引用上一条时应一并带上。
  • 人类版本的同一件事（[00:11:06]）："人之间也有这种事：你卡在某个方法上，跟另一个人讲讲你的大致想法，他回来就搞定了怎么让它 work。只是人做这件事要花更多时间。"

三、训练数据：主持人提出的那个反问

⚠️ 这一节的问题由主持人提出，OpenAI 一方的回答很短。本库把问题与回答分开记。

  • 主持人的论证（[00:11:06]–[00:12:06]）：数学论文与教科书先验地是很差的训练集——
  • "别从 Rudin 学实分析"：它已经太干净、太清爽了。
  • 这很糟糕，因为它不展示那些让我们以某种方式形成定义的挣扎——"为什么实数要被定义成这么抽象的样子"。
  • 论文也一样：大多数人写论文时并不带着"我要把某个人教成数学家"的上下文，所以"学数学的真正课程，并不内在于我们数学家留下的那些制品里"。
  • ⚠️ 她后面还把它与代码做了对比（[00:14:08]）：代码是很好的语料，因为它是少数具有极大上下文、且结构上高度互联的数据集之一；而"我们在 coding model 上仍然做不好的，恰恰是那个数据集不包含的东西——语法在那里，但更高层的语义、'为什么我必须这样写'不在那里"。
  • OpenAI 一方的回答（[00:13:07]）：他们训练的是通用推理模型；回溯、重开这些行为"并不真的是数学特有的"——"我们是在数学的这些例子里看到它们，但它们是推理的通用工具"；"如果你在推理上下足功夫，最终就该看到这些模式。"
  • ⚠️ 主持人点出的路线分野（[00:13:07]）："OpenAI 的路子之所以让人印象深刻，是它不依赖做自动形式化来引导推理"——而那条路"显然更像我们（人类）"。本库把这条记为与 Lean/形式化验证路线的明确分野，可与 Greg Brockman 说把 Navier–Stokes 形式化进 Lean 并读——那是把结果形式化以做验证，不是用形式化来引导推理，两者不矛盾。
  • ⚠️ 他们为什么要公开摘要版思维链（[00:15:09]）："如果你从没见过这些，只看到一堆证明冒出来，你不知道这意味着什么——模型是不是在以某种疯狂的方式瞎猜？它是不是在用某种完全陌生的方式思考？" 而实际上——"它的推理方式，震惊地像一个专家人类。"
  • 他们给的阅读体感（[00:15:09]–[00:16:09]）："很像在读一位同事的笔记"，只是更零散一些——"尤其当你和合作者足够熟，有时他们就会把想法直接倾泻在一封邮件里给你，读起来就像把很多这样的邮件串在一起"。"头几次相当令人惊讶。"

四、结果一：球填充（Astra 那十个问题中的第一个）

⚠️ 本节的数学背景由两位嘉宾在白板上口述，本库按其口述整理；具体数值形式的转录问题见页首。

  • 问题（[00:16:09]–[00:17:12]）：d 维空间里半径为 1 的球能填得多密？
  • d=1 不是有趣的问题（实数轴，能铺满）。
  • d=2 是那个大家都喜欢的图——六边形格。⚠️ 主持人问"这是显然的吗"，回答是"不那么显然，我想是 1960 年代才被证明的；有一个简短的论证，但不容易"。
  • ⚠️ 他们对直觉的坦率回答，本库认为是本页最好的一句（[00:17:12]–[00:18:14]）："这个问题最棒的地方就是，真的没有人有任何直觉。" 接着是："老实说我对它最好的直觉是——蜜蜂就是这么做的。如果有更高效的方式，蜜蜂大概会用别的方式堆蜂巢。"
  • d=3 就是杂货店堆橙子的方式，Hales 在 2000 年代证明，最短的证明也有几百页——"大量线性规划论证 + 非常精细的几何，其实相当丑，是一个著名地丑的论证"。
  • d=8 与 d=24 在 2017 年被解决，靠的是两个特殊的格——E8 与 Leech 格——"它们非常漂亮、异常地密，是来自数学其他领域的漂亮结构，而结果证明它们就是最优结构"。（⚠️ 他们提到 Viazovska因此在 2022 年获菲尔兹奖。）
  • 此外一个精确维数都不知道："我们知道这五个维数，别的基本什么都不知道。"
  • 已知的上下界（[00:19:15]–[00:21:16]）：
  • 下界 2^(−d)，论证很漂亮也很短：取任何一个"再也放不下第二个球"的填充；把每个球放大两倍，它们必须覆盖全空间——否则哪里有空隙你就能再放一个球。
  • 上界必须指数衰减——高维里只能覆盖消失般小的一部分。他们插了一个相关的怪事实（[00:22:16]）：高维立方体的每个顶点各放一个球，中间还能再塞进去一个球，而且塞得下。
  • 长期以来最好的界约为 2^(−0.599d)，由两位俄国数学家在 1970 年代证明（⚠️ 姓名转录不清，见页首）。⚠️ 他们提到那篇论文只有一两页、细节很少、而且很难找到。
  • Cohn–Elkies 的线性规划框架（[00:24:18]–[00:25:20]）：构造一个函数 f: R^d → R，满足两个条件——当 |x| > 1 时 f(x) ≤ 0，以及 f 的傅里叶变换处处非负。因为傅里叶变换是线性算子，这就是一个（无穷维的）线性规划。满足这两条的任意 f 都给出一个上界（由 f(0) 与其傅里叶变换在 0 处取值的比值，乘以半径 1/2 的球的体积）。
  • ⚠️ 这是一个松弛问题——"没有保证取最优的 f 就能给出 δ_d 的好界"。
  • Viazovska 的工作（[00:26:20]）：在 8 维和 24 维构造出使这个上界恰好等于那两个特殊格的函数——"这既能构造出这个函数、又恰好给出最优界，是自然的奇迹"。
  • 此前的猜想（[00:26:20]）：Cohn 等人的一篇数值论文猜出了大维数下的答案，"但他们完全不知道为什么会是这个答案"。
  • ⚠️ Astra 做了什么（[00:26:20]–[00:28:20]）：
  • 证明这个线性规划界在大维数下有一个非常漂亮的渐近行为，且证明解释了它是从哪来的。
  • 因为把 LP 界彻底搞清楚了，这直接给出 δ_d 的一个更好的界；旧的那个界可以在这个框架里被重新解读。
  • 最强的一点：它先构造出给出这个界的 f，再证明没有任何 f 能做得更好——"所以这是一个等式，相当强。我们现在对这个高维问题理解得很好了。"
  • ⚠️ 给模型的指令："分析这个高维线性规划，去玩得开心。"
  • 他们自己的反应（[00:28:20]）：
  • 一位说自己研究生时在这个问题上花了大约半年、"零进展"，所以"被解释为什么它是对的，是一次愉快的体验"。
  • 另一位给的评价更具体："LP 不可能做得更好"那部分的模型解法"相当短——几页复数分析，但方式恰好是对的"。他的感受是——"一旦你看到它，你会觉得难以置信：为什么以前没人做过这个？" 并加了一句："好数学有很多种，其中一种就是你看到它然后想'天哪，我怎么没想到'。"

五、结果二：球面码与二元码，以及唯一一次交互

  • 对象（[00:29:21]–[00:32:25]）：
  • 球面码就是在另一个球面上做球填充（同一张图，只是在曲面上）。
  • 二元码是同样的东西但在立方体上——也就是纠错码。定长二进制串就是超立方体上的一个点，而你要一本彼此分得足够开的码字词典（Hamming 距离足够大）。
  • ⚠️ 他们给的直觉类比：普通英语就有这个性质——你打几个错字，对方还是能看懂你的意思；而一个脆弱的通信方案就不行。
  • 实际问题的形式（[00:32:25]）：如果我发一个 n 比特的串、有 1% 的错误率，我的消息得变长多少才能容忍这些错误——这是通信的一个基本信息论极限。
  • 两者的联系（[00:32:25]）：如果你把这些小球做得非常小，那个大球的曲率就不太要紧了，它看起来就像在全空间里填球。
  • ⚠️ 技术路线不同这一点值得单记（[00:33:27]–[00:34:28]）：全空间那个线性规划的分析用的是复数分析；而码的这两个情形用的是表示论——因为球和立方体都有大量对称性，关键改进是把代数对称性以更精巧的方式引入、"在表示论上狠下功夫"。而且从表示论的公式里取球面码的"小球极限"，能恢复出全空间那个结果的一部分。
  • ⚠️ 十个问题里唯一一次交互式的过程（[00:34:28]–[00:35:28]）：
  • 先让它改进码的界——它回来给了一个用到一定表示论的改进。
  • 他们问："你能不能再往前推一点，看看会怎样？"——它回来给了复杂得多的表示论，而且把那个方法推到极限时，顺带得到了全空间球填充的那个猜想值。
  • 于是他们直接让它分析全空间的情形，把整幅图补完。
  • ⚠️ 他们对"第一次为什么没推到底"的解释，本库认为是本期关于模型行为最有信息量的一条（[00:36:29]–[00:37:29]）：最初给码的任务是"把界改进某个指数因子"，它改进了，"就没再多推。有时候你看到它会推，有时候它就是不费那个劲。所以这不是能力问题——它当时就是不想。" 归纳成一句："模型相当任务导向。你让它做一个任务，它完成了，它就挺满意的。"

六、关于"品味"（taste）与 harness 的讨论

⚠️ 本节大部分推演来自主持人，OpenAI 一方的回答较短。本库分开记。

  • 他们给的品味定义是功利主义的（[00:39:29]）："如果你能靠做出更好的判断更快地解决问题，那就是我对品味最好的一般代理。而解决更难的问题，按定义就意味着它有更好的品味。"
  • 他们承认的那个症状（[00:39:29]–[00:40:31]）：偶尔你会看到它明显做出了突破、它也理解自己做出了突破，然后它没有把事情推到极限，因为那不是你要求的——但"跟我们已经看到的进展状态相比，这似乎相当次要"。
  • ⚠️ 他们提出的分工方案，本库认为是本期最该被 AI for AI 与自动研究 引用的一条（[00:40:31]）：

    "如果你有一个模型负责品味，另一个模型负责出去长时间干活解决一个难问题——作为那个监督 AI 的下属——我觉得目前这样会挺好的。"

    理由是：当你同时要做一个具体的长时程任务、又要展现品味时，你容易搞混。⚠️ 主持人当场指出这其实是一个更强的主张——它意味着这两件事即便不是分离的，至少不该互相污染对方的上下文。

  • 人类类比（[00:42:31]–[00:43:31]）："做任何任务时你偶尔会钻牛角尖、拼命干；而只要有个朋友探头过来问一句'你在干嘛'，就那一比特的、退后十秒的提醒，往往非常有用。" 落点是——"我看不出人为什么会和模型有那么大不同"，以及 "几个人一起干活往往比一个人更强"。
  • 他们给的品味的第二个成分（[00:43:31]）："对'你或你手上的某个方法擅长解决什么问题'有一种嗅觉"——"为了能取得进展而对该追什么有鼻子"。他们认为这应该会作为"擅长完成任务"的副产品出现。
  • ⚠️ 关于任务长度的一条判断（[00:38:29]）："解决一个更难的数学问题，就是要解决许多更小的、没那么难的数学问题；而数学问题正在变难这件事，本身就说明模型能在一个连续的单元里承担越来越多的工作。" 配套的观察是：这些解法都不是"一个想法然后一路通关"，而是需要好几块东西互相作用、互相对话。
  • 主持人关于 harness 的一段推演（[00:36:29]、[00:41:31]–[00:42:31]）：她指出应用 AI/创业公司里"你需要 harness，但 harness 对新模型适应得很差"，有时极简的 harness 反而是暴露模型原始能力的最好方式；而现在又出现了要求 harness 与训练绑在一起的训练机制——她猜一部分动机是保持专有性，一部分是对你在意的推理轨迹有更多控制。⚠️ OpenAI 一方没有正面回应这一段，本库照录这处不回应。

七、结果三：存在非 sofic 群

  • 背景（[00:44:32]–[00:48:40]）：
  • 群是带乘法运算的元素集合，是数学家思考对称性的方式。群可以是有限的（正方形的旋转，4 个元素）或无限的（圆的旋转，不可数多个）。
  • sofic 群是有限或可数的（应当想成可数无限，元素个数和整数一样多）群，且在某种意义上可以被有限群逼近。
  • 整数为什么是 sofic 的（[00:49:46]–[00:50:47]）：把整数画成图（连接最近邻），而整数模 n 给出的是同一幅图，只不过是个大圆而不是无限长的线——近处看起来完全一样，你得走得非常远才能看到"这是圆不是线"这个全局几何结构。所以整数模 n 就是整数的 sofic 逼近。
  • 为什么有人希望所有群都是 sofic 的（[00:47:36]）：因为这样的群有很多好性质——你可以对有限群跑某些证明，然后按 sofic 的定义去逼近，把结果拿过来。他们把这个希望说成"人们盼着有个奇迹"。
  • 具体动机（[00:48:40]）：任何 sofic 群也是 surjunctive 的；而"是否每个群都是 surjunctive"是 Gottschalk 在 1970 年代的问题——正是这条"先对有限群证明、再做逼近"的模式，催生了"是否存在非 sofic 群"的问题。
  • ⚠️ Astra 的结果（[00:46:36]）：存在一个非 sofic 群。
  • ⚠️ 与 Aldous–Lyons 猜想的对照，本库认为是本期最强的量化对比（[00:48:40]–[00:53:51]）：
  • Aldous–Lyons 猜想更强（概率领域）：任何具有 unimodularity 的无限随机图都能被大的有限图逼近。它更强是因为它允许更广的一类图——允许随机图，而不只是从群的 Cayley 图得到的确定性图。
  • 它在大约两年前被证伪，用的是约 250 页、建立在另外约 200 页之上的 tour de force 工作，动用了量子复杂性理论——"它搭了一座非常复杂的桥，我想没有多少人能看懂"。
  • ⚠️ 而"存在非 sofic 群"的直接证明短得多也容易得多——"大概 15 页吧，完全没有那种与量子复杂性的复杂联系，就待在群论的地界里"，只用到了别的数学家已有的一些重要结果。"它就是一个非常合理、普通的证明。"
  • 难在哪（[00:53:51]–[00:54:52]）："是 sofic 群这个性质不太好下手"——你必须找到一个具体的说法来说'这个群不可能是 sofic 的'。证明很短，几乎是一个组合论证，但是极其精细的组合论证；而模型既要有正确的陈述、又要知道文献里哪些零件可用、还要正确地执行。
  • ⚠️ 他们做了 postmortem，而答案是本页最有意思的一段（[00:54:52]–[00:55:52]）：他们直接问 Astra"解释给我听"。答案是存在一个具体的组合障碍——如果你去读之前那些论文，你会意识到那正是前人无法排除的东西；而 Astra 找到的办法是"加上这一条额外的代数事实，这个奇怪的阴谋就不可能发生"。他们的评语是：

    "它非常明显是在排除前人隐约写到过的那个 conspiracy……而那些确实就是真凶。所以他们本来就在正确的轨道上，这件事做完了最后一英里。"

  • ⚠️ 由此归纳出的那条一般模式（[00:53:51]、[00:55:52]）：见概要第 1 条。

八、数学共同体怎么接住这些结果

  • 已经在发生的后续（[00:56:53]）：被这个证明所依赖的那两位数学家已经做了后续工作（⚠️ 姓名转录不清），给出了更多非 sofic 群的例子。OpenAI 一方的态度很明确："我们不想自己写一堆后续论文；如果有人接着这些想法往下建，我们非常非常高兴。"
  • 主持人描述的光谱（[00:56:53]–[00:57:55]）："现在大多数人大概是：好吧，AI 显然在做一些非平凡的事情，不把它放进我的工作流会是一种劣势。" 但她也听过一些故事——有人很难接受把 AI 当合作者，或者不知道该怎么做署名。⚠️ OpenAI 一方没有回应署名问题，本库照录这处不回应。
  • ⚠️ 他们给的那条"它也在解决它自己制造的问题"，本库认为是本期最值得单独引用的乐观论证（[00:57:55]–[00:58:56]）：

    模型既然能产出复杂的数学，就能帮你理解复杂的数学。

    他给的具体用法很朴素：翻 arXiv 时想搞懂某个证明，读引言当然可以，但实际上把 PDF 丢进自己最喜欢的模型、让它给出大致的证明策略要快得多。落点是——"模型当然会让我们产出指数级更多的数学，但它们也让吸收这些数学容易得多……所以它反正在解决它自己制造的那个问题。" 他补了一句限定："现在还是有点来回折腾，但对我来说，有模型理解一段数学比没有模型快得多得多。"

  • ⚠️ 瓶颈迁移，本库认为这是本页最该被 AI 与就业 引用的一段（[00:59:56]–[01:00:56]）：
  • 一个结果要成立，需要有人想出它，但也需要有人理解它、吸收它、内化到足以用它做更多事，并弄清它在人类理解的版图里落在哪。
  • ⚠️ "几年前，证明这件事本身太难了，以至于其他那些事基本上是搭便车来的"——如果你自己证出来了，你自动就很好地理解了它，某种意义上你也就对维护它、向别人解释它负责。
  • 现在，从前的主要瓶颈不再是瓶颈了，于是那些别的约束开始起作用——"组织知识的最优结构，可能会看起来相当不同。"
  • 他们对职业形态的预测（[01:01:56]）："把它放进一个恰当的框架里、能把它解释给其他人听，让他们也能欣赏"这件事——"某种程度上我们一直隐含地看重它，但那通常是因为证出结果的人顺便给了所有人理解"；而往后这会越来越多地取决于"你是那个能把理解交给别人、并帮他们用起来的人"。落点是：

    "这种共同体层面的理解，过去在我们看待数学的方式里更多是隐含的；我认为它会变成这门学科里越来越显性、也越来越有价值的一部分。"

  • ⚠️ 他们给的天花板论证（[01:01:56]–[01:02:56]）："数学问题的难度上限相当高。所以即便 AI 在数学上继续以指数方式变好，也完全有可能我们永远解不出 P vs NP 这样的东西。" 推论是这门学科可能变得更贴近那些大谜团，而更少贴近那些偏例行公事的小谜团。
  • 两条更个人的收尾：
  • "有些事我花了几个月甚至几年去想、从没想明白……其中一部分我将会知道答案了。我对此挺开心的。"（[01:02:56]）
  • ⚠️ 访问门槛的变化（[01:03:56]）："如果你在做某件需要一点数学的事，你突然不需要去找到这个题目的世界级专家才能把它用进自己的工作。" 以及全期最后一句实质表述——"如果应用数学能快很多，对这个世界会是好事。"

与本库其它观点的关系

  • AI for Science：本页是该页第一份来自前沿实验室内部、且给出可核查结果清单的材料。⚠️ 它与 Greg Brockman 提到的 Navier–Stokes 应当并读——Brockman 那条没有说清是哪个 Navier–Stokes 问题，本页则给出了三个有名有姓的结果（球填充的 LP 渐近、球面码/二元码的新界、非 sofic 群的存在性）与各自的技术路径。"AI 的证明普遍很短很优雅，而人类才产出 200 页证明"是该页此前完全没有的一条经验规律。
  • AI for AI 与自动研究："一个模型负责品味、一个模型负责长时程干活"这条分工提议，以及"任务变难说明模型能在一个连续单元里承担更多工作"这条尺度判断，是该页的新条目。⚠️ 与 Ryan Greenblatt 那期 对照读时要注意：本页谈的是数学这一个已有可验证信号的领域，不能直接外推。
  • LLM 心理学："模型相当任务导向——完成了任务它就满意了，不推到底不是能力问题"，以及"上下文污染"作为人类相对于 AI 的结构性劣势，是该页迄今最具体的两条行为观察。⚠️ 同时应记住他们自己的削弱——部分优势可能只是来自"能重开一个 session"。
  • LLM 训练流水线："我们训练的是通用推理模型，回溯与重开不是数学特有的"，以及不依赖自动形式化引导推理这条路线选择，是该页关于推理训练的新条目。主持人那条"数学论文与教科书先验地是很差的训练集，因为它们已经太干净、不展示挣扎"是一条值得单独保留的反面论证。
  • AI 与就业：瓶颈从"证出来"迁移到"理解、吸收、解释"是本库第一条来自专业学术领域内部的岗位价值重排论证。它与 苏廷浩描述的"学习成就感被抹平" 指向同一现象的两端——一端是高中生失去学的理由，另一端是数学家发现"解释"成了新的稀缺。本库认为这两条应并列读。
  • 实践中使用 LLM："把 PDF 丢进模型拿证明策略，比读引言快得多"是一条极具体的专业用法；"五分钟找到一篇我和朋友花几小时都没定位到的文献"是另一条。
  • 评测与基准："数学问题的难度上限相当高，即使指数级变好也可能永远解不出 P vs NP"是一条罕见的、来自实验室内部的能力天花板表述。
  • a16z：⚠️ 本期主持方的发言占比异常高，且多为长段落的自我推演（训练数据的批评、harness 与 taste 的关系）。本库把本期记为该频道少见的"主持人提出了嘉宾没有正面回答的若干问题"的一期——署名问题、harness 与训练绑定的动机，两处 OpenAI 一方都未回应。