跳转至

OpenAI 数学团队（两位研究员）

  • 背景: 两位转行前的执业数学家，2026 年先后加入 OpenAI，工作内容是把开放数学问题喂给模型、读它的思维链、判断结果的成色。两人此前是长期合作者，合写过论文。
  • ⚠️ 姓名：转录稿（自动字幕）写作 Mark Selki 与 Matab Swani。疑为 Mark Sellke 与 Mehtaab Sawhney（两位均为知名的概率/组合数学家），但本库不作确证——自动字幕的人名拼写不可靠，本页凡需指称处一律用"两位数学家"或转录稿给出的名字形式。
  • 本库中的位置：本库第一份来自前沿实验室内部、专门谈 AI 做数学的一手材料。此前 AI for Science 的来源是应用侧 neo-lab（Lila Sciences、Xaira、Genesis Molecular AI）或领导层转述（Greg Brockman）。
  • 首次收录: a16z，2026-09-08

⚠️ 本页在两位之间基本不做区分——自动字幕无姓名标签，两人语流高度交错、互相接话补完。仅两处有明确锚点：先加入的那位是 Mark（去年夏天看到 IMO 金牌后加入）；讲 Erdős 问题站那段经历的是 Matab（组合数学背景）。

立场与关注点

一、最该被记住的一条：AI 的证明普遍很短

  • ⚠️ 他们说这与自己的预期相反（[00:55:52]）："一年前我会非常惊讶地得知这些 AI 证明都很短、很优雅。你原本担心它会生成一堆千页的东西、你永远看不懂——但结果恰好相反。"
  • 配套的那句更尖锐："目前只有人类能产出 200 页的证明。"
  • 最强的量化对照（[00:51:50]–[00:53:51]）：更强的 Aldous–Lyons 猜想两年前被证伪，用了约 250 页、建立在另外约 200 页之上、动用量子复杂性理论的工作，"没有多少人能看懂"；而 Astra 证明"存在非 sofic 群"的证明约 15 页，完全待在群论里。

二、AI 的相对强项与人的相对劣势

  • 强项一：对文献的熟悉（[00:03:02]、[00:05:03]）。触发 Matab 转变的正是这件事——他把一个 Erdős 网站上标着 open 的问题丢进 GPT-5，五分钟后它找到了文献，而他和朋友已经为此花了几小时还不确定问题是否够得着。他们随后又找到十来个类似案例。
  • 强项二：细节执行（[00:05:03]）："每当你有一个想法，总要把一堆东西对齐……人很容易在这些细节里迷失，而 AI 总是把这类论证钉死。"
  • 强项三：敢下不划算的注（[00:06:03]–[00:08:05]）。人的常态是试几小时/几天/几周然后放弃，因为风险回报不划算；而一两年后发现别人把你以为不成的想法做成了，是并不罕见的经历。结论："把一个想法做成，本身就可能是战役的一大部分。"
  • ⚠️ 人的核心劣势是"上下文被污染"（[00:09:05]）：人沿错路走一阵后很难重新布线——"你的 context window 有点被污染了，而你没法从上周的自己再克隆一份出来"。
  • ⚠️ 他们自己削弱了"模型判断更好"这条（[00:10:06]）：他们先说模型更善于更新"某条路径成功的概率"，随即补一句——即便不是这样，光是"可以重开一个 session"就够了。本库认为引用前半句必须带上后半句。

三、模型在思维链里表现得像什么

  • 为什么公开摘要版思维链（[00:15:09]）：不公开的话，"你不知道模型是不是在以某种疯狂的方式瞎猜"。而实际上——"它的推理方式，震惊地像一个专家人类。"
  • 阅读体感（[00:15:09]–[00:16:09]）："很像在读一位同事的笔记"，只是更零散——像把同事倾泻思路的一堆邮件串在一起。
  • 剪枝而非穷举（[00:08:05]）："它并不是在试所有东西。它试了很多不同的东西，它极其执着，但它不可能试每一个想法"——靠知道几个非常正确的小事实做出正确决策。
  • ⚠️ 最有信息量的行为观察（[00:36:29]–[00:37:29]）："模型相当任务导向。你让它做一个任务，它完成了，它就挺满意的。" 十个问题里唯一一次追问"你能不能再往前推一点"之后，它给出了复杂得多的表示论——"所以这不是能力问题，它当时就是不想费那个劲。"

四、品味（taste）与分工

  • 定义是功利主义的（[00:39:29]）："如果你能靠做出更好的判断更快地解决问题，那就是我对品味最好的一般代理。解决更难的问题，按定义就意味着更好的品味。"
  • ⚠️ 他们提出的分工方案（[00:40:31]）：一个模型负责品味，另一个模型作为"下属"出去长时间干活解决难题——理由是同时做具体长时程任务又展现品味容易搞混。⚠️ 主持人当场指出这其实是一个更强的主张：两者的上下文不该互相污染。
  • 人类类比（[00:42:31]–[00:43:31]）："有个朋友探头过来问一句'你在干嘛'，就那一比特的退后十秒，往往非常有用"——"我看不出人为什么会和模型有那么大不同。"
  • 任务长度的判断（[00:38:29]）："数学问题正在变难这件事，本身就说明模型能在一个连续的单元里承担越来越多的工作。"

五、训练路线：通用推理，不依赖形式化

  • ⚠️ 他们的回答（[00:13:07]）：回溯、重开这些行为"并不真的是数学特有的"——"它们是推理的通用工具，如果你在推理上下足功夫，最终就该看到这些模式"。
  • ⚠️ 主持人点出的分野：这条路线不依赖自动形式化（Lean 一类）来引导推理。本库把它记为与形式化验证路线的明确分野——注意 Brockman 说把 Navier–Stokes 形式化进 Lean 是用形式化做验证，不是用它引导推理，两者不矛盾。

六、他们对数学这门职业的判断

  • ⚠️ 瓶颈迁移（[00:59:56]–[01:00:56]）："几年前，证明这件事本身太难了，以至于其他那些事基本上是搭便车来的"——你证出来了就自动理解了它、也就负责解释它。现在主要瓶颈不再是瓶颈，别的约束开始起作用，"组织知识的最优结构，可能会看起来相当不同"。
  • 对职业形态的预测（[01:01:56]）：共同体层面的理解——"你是那个能把理解交给别人、并帮他们用起来的人"——"过去更多是隐含的，我认为它会变成这门学科里越来越显性、也越来越有价值的一部分"。
  • ⚠️ 天花板论证（[01:01:56]）："数学问题的难度上限相当高。即便 AI 在数学上继续以指数方式变好，也完全有可能我们永远解不出 P vs NP 这样的东西。" 推论是这门学科可能变得更贴近大谜团、更少贴近例行公事的小谜团。
  • ⚠️ "它在解决它自己制造的问题"（[00:57:55]–[00:58:56]）：模型既然能产出复杂数学，就能帮你吸收复杂数学——把 arXiv 的 PDF 丢进模型拿大致证明策略，比读引言快得多。
  • 访问门槛（[01:03:56]）："如果你在做某件需要一点数学的事，你突然不需要去找到这个题目的世界级专家。" 落点是——"如果应用数学能快很多，对这个世界会是好事。"
  • 他们希望共同体接手（[00:56:53]）："我们不想自己写一堆后续论文"；被 Astra 证明所依赖的那两位数学家（⚠️ 姓名转录不清）已经做出了后续工作，给出更多非 sofic 群的例子。

七、三个结果（摘要）

详细背景、技术路径与他们各自的反应见视频页第四至七节。

  • 球填充的线性规划界（[00:23:18]–[00:28:20]）：Astra 给出大维数下 LP 界的渐近行为并解释了它的来源，由此改进了填充密度的上界；且证明不存在更好的函数 f——是一个等式。给模型的指令基本就是"分析这个高维线性规划，去玩得开心"。他们的评语："一旦你看到它，你会觉得难以置信：为什么以前没人做过这个？"
  • 球面码与二元码（[00:29:21]–[00:35:28]）：技术路径与上一个完全不同——全空间用复数分析，码的情形用表示论（利用球与立方体的对称性）。⚠️ 这是十个问题里唯一一次有交互的，而交互内容只是"你能不能再往前推一点"。
  • 存在非 sofic 群（[00:46:36]–[00:55:52]）：证明约 15 页、几乎是一个极其精细的组合论证。⚠️ postmortem 最值得记：Astra 指出存在一个具体的组合障碍，正是前人论文里隐约写到却无法排除的那个——"加上这一条额外的代数事实，这个奇怪的阴谋就不可能发生"。他们的评语："那些确实就是真凶。前人本来就在正确的轨道上，这件事做完了最后一英里。"

相关页面