# Robinhood创始人再创业：直接教AI学数学，把黎曼猜想押在2029 > Training Data No. 16 中文精读 - 原标题：Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math—and Why It Matters - 发布日期：2024-09-24 - 主持：Sonya Huang · Pat Grady · Konstantine Buhler 等 - 网页版：https://trainingdata.qiaomu.ai/ep/016-why-vlad-tenev-and-tudor-achim-of-harmonic-think-ai-is-about-NvAxuC.html - 精读字数：约 5295 字（阅读约 12 分钟） > 本文为 trainingdata.qiaomu.ai 基于原始访谈的 AI 改写中文精读，非官方翻译；引用请注明出处并链接网页版。 预测平台Metaculus上挂着一个问题：下一个千禧年大奖难题，会不会由AI解决，或者由人类在AI重度辅助下解决？截至这期节目录制，市场给出的概率是43%。Metaculus是个给预测者打分的平台，这个数字是众多预测者真金白银交易出来的。 觉得43%还太低的人，叫Vlad Tenev。他的身份是Robinhood创始人兼CEO，另一个少有人知的身份：斯坦福数学系毕业，UCLA数学博士退学，导师是陶哲轩。**他的判断是，如果下一个千禧年大奖还被纯人类拿下，那必须发生在很近的将来；再下一个，几乎肯定会有AI的深度参与。** 这次他拉着联合创始人Tudor Achim开了一家叫Harmonic的AI研究公司，目标写得很直白：造出数学超级智能，用数学撬动更广泛的推理能力。红杉资本的播客Training Data把两人请来聊了一期，主持人是Pat Grady和Sonya Huang。整期节目的核心就一句话：为什么他们赌「数学即推理」，并且要用最直接的方式把数学教给AI，别的公司则在等数学能力从规模里自己涌现。 ## 数学好的人，干什么都快 Harmonic的核心信念只有五个字：数学即推理。Tudor的论证很朴素：几乎所有科学和工程学科，底层都是数学。从黑洞到原子，物理现象靠数学建模，工程设计靠数学推演。宇宙恰好能用一套紧凑的符号系统来解释，而数学给了人类一种客观、透明、可共享的思考框架：先约定演绎规则，再一步步推出结论。 所以他们的赌注是：**把AI的数学能力做到顶尖，它在科学和工程任务上的表现会跟着起飞。**可能暂时写不好历史作文，但让它做科研、做工程，会非常强。 Vlad拿自己现身说法。小时候数学课上总有同学举手问老师：「这玩意儿什么时候用得上？」老师的回答含含糊糊：你大概率用不上，但它会让你别的科目也变强。Vlad信了，一路读到斯坦福数学系，又去读博。抽象代数的习题集，他每周对着墙撞十个小时。后来创业，编程捡起来很快，合同也能自己读懂。他的原话大意是，数学训练迁移到了「其他很能赚钱的事情上」，他自己就是活例子。 Tudor补了一个行业内的公开秘密：**用大量代码数据训练模型，会明显提升推理基准的成绩。**代码尚且如此，覆盖面更广的数学数据集会是什么效果，可以自己推。 ## 陶哲轩签了名的那本书，再也拿不回去了 聊到陶哲轩，Vlad的话明显多了。他的评价是：大多数数学家只在一个狭窄领域钻得很深，陶哲轩能在几十个领域都做到顶尖，数论、组合数学、调和分析、应用数学都有他的贡献。现在他还在给Lean做贡献，把自己的论文形式化，泡在社区的Zulip论坛里跟学生互动，博客也一直没停。 原因？Vlad的答案很直白：他比99.999%的人都聪明，可能还不止。国际数学奥林匹克的老照片里，澳大利亚队的高中生们个头很高，站在中间的陶哲轩小了一大圈，还是队长。很小的时候，他就已经在另一个层面上做题了。 Vlad读本科时的荣誉论文导师是Larry Guth，也是位狠人，最近刚在黎曼猜想相关的问题上拿出了突破性结果，靠的还是传统数学工具。Vlad的感慨是，人类如果还能抢下一个千禧年大奖，大概率就是很近的事，也可能正是Guth这条路。当年是Guth建议他去UCLA的。结果他在UCLA只读了一年就退学创业，但他坚持认领「辍学生」这个身份：毕竟是博士辍学，含金量不一样。 那一年里有个段子。陶哲轩借给他一本书，还签了名，用意大概是确保这学生读完记得还。签名的作用恰恰相反：这本书从此留在了Vlad的书架上，和其他签名初版书摆在一起。他说每次和陶哲轩吃饭都要提一嘴：那本书你别想要回去了。 顺便说一句，吃饭不聊股票。上市公司CEO不能交易自己领域的股票，听到的内行观点只能烂在肚子里。Vlad说自己热爱交易，现在基本不能碰，挺遗憾的。 ## Lean：一个软件工程师写的语言，成了数学界的顶流 Harmonic的技术底座是个叫Lean的编程语言。创造者里奥纳多·德·莫拉（Leonardo de Moura）现在在亚马逊AWS，他本人根本不是数学家，最初的目标是做软件验证工具。他的判断是：未来的软件应该被证明正确，而Coq、Isabelle这些老牌验证工具开发者体验太差，基本没法用。做个更好的，用的人多了，软件质量自然上去。Vlad在旁边插了句：这是最好的编程语言。 原理说穿了不复杂。Lean把数学命题编码进类型系统：函数的输入类型对应定理的前提，输出类型对应结论。**只要你写出的程序能通过编译，就等于证明了「从前提能推出结论」。**证明即程序，编译即验证。 有意思的转折在这里：德·莫拉想做的是软件验证，结果数学社区先疯掉了。几千名数学家和学生在上面添砖加瓦，攒出一个叫mathlib的开源库，可以理解成一本还在快速变厚的、世界上最大的数学教科书，就摆在GitHub上。Vlad说，Lean在数学圈的使用量，搞不好已经超过了它在软件验证上的使用量。 Tudor特意泼了盆冷水：Lean只负责判断对错。**它不会告诉你离答案还有多远，也不会告诉你模型有没有变聪明。**怎么让系统快速变强，中间还有一堆开放的科学难题。 ## 为什么是现在：数据墙逼出来的路线 强化学习几十年前就有，数学更是几千年的老学科，为什么偏偏现在创业？Tudor给了两个时间点。 第一，自回归语言模型成熟了。2015、2016年他就跟朋友聊过用强化学习做定理证明，当时卡在一个基本问题上：围棋里AI只需要预测「黑子还是白子落在哪」，选项有限；数学里下一步可以是任何东西，动作空间无限。那个年代没有模型能处理这种问题，现在有了。 第二，Lean自己变强了。二十年前你跟数学家说，这行的大多数人会对形式化方法兴奋，他大概觉得你疯了。那时候形式化方法只活在数理逻辑和一小块图论里，四色定理的机器证明算是最出名的成果。转折点是mathlib攒出了足够的知识储备，加上Lean 4在2023年9月正式发布。AI能干了，教材也齐了，两件事撞在一起，时机就到了。 数据策略上，Harmonic走的是合成数据路线。mathlib是人类写的，风格紧凑、偏理论，适合查定理，不适合拿来练解题。Tudor的原话：这几乎是AI领域里数据最贫瘠的分支。主持人Sonya Huang调侃：互联网上的数学数据，就是没有猫视频多。所以**训练信号主要靠一群智能体分头做题来生产：解出题，Lean判定对错，对错变成奖励，奖励变成数据。**先证简单的定理，再一级级往上放大。 Vlad把「数据墙」拆成了两层。一层是大家都在说的：互联网的文本快用完了。另一层更致命：猫视频和维基百科的水位，决定了模型聪明程度的天花板，喂这些东西训练，很难长出远超人类的能力。想超过人类数学家，必须进入自我对弈、自我强化的循环，走AlphaGo到AlphaZero那条路，让模型自己生产绝大部分训练数据，而且数据难度随迭代不断上升。 数学在这条路上有个天然优势：题目难度可以用Lean代码行数来度量。一道大题拆成小块，每块需要更少的行数，模型先把小块做熟，再回头啃大题，难度螺旋上升。这跟人类在草稿纸上解题的方式一模一样。费马大定理的证明大约两百页，黎曼猜想估计要几百页起步。Vlad有句话很妙：**数学某种程度上就是最早的合成数据，人类从几条公理出发，推了几千年，堆出了整座大厦。** 那进步速度由什么决定？Tudor给的答案很硬核：能量。算力越多，并行尝试越多，数据生产越快，没有根本性的速度上限。Vlad补充了两个现实约束：mathlib还不完整，几何内容少得可怜；另外模型得学会自己创造新理论、把人类没形式化的东西自动形式化。他举了个例子：拍一段棒球队传接球的视频，系统直接把它变成Lean代码。这事现在还不可靠，但一旦可靠，会是个巨大的解锁，他预计就在未来几年内。 ## 数学界吵起来了，棋盘给出了答案 数学圈怎么看AI做题？Vlad的回答：分裂。年轻数学家拥抱AI和Lean，老一辈普遍怀疑，跟所有行业的新旧交替一个剧本。 Vlad的心理模型是国际象棋。先经历一段人机协作期，人类搭着AI的便车出很多好成果；AI越强，人类的输入就越多余。今天的国际象棋已经是这样了：**AI要是能吐槽，它会把人类建议全部删掉，因为只会拉低棋力。**数学会不会走到这一步，他不确定，但数学家这个职业的定义肯定要变。 他问过MIT一个年轻数学教授，你慌不慌，你这行要被改写了。对方回了一句：「数学这个行业从来就没停止过变化。」十九世纪的数学家待在宫廷里，本质上是体面的计算器，靠手算二次方程吃饭。计算器出来时他们也慌过，后来呢？数学是什么，由数学家自己定义。 > 「就算AI证明了黎曼猜想，人类也永远在环节里，因为黎曼猜想本来就是人类提出来的。」 Tudor补了更具体的一层：未来会有大量算力投向数学，真正人类的问题是，用什么流程决定把这些推理火力往哪指。选什么题、怎么解读结果、怎么从失败里读出信息，这是未来数学家的日常工作。 黎曼猜想本身能不能被AI拿下？Vlad认为可以，还有一种同样有趣的可能：证明它不可判定。他观察陶哲轩这类顶级数学家的工作方式：大量综合前沿论文，找到别人看不见的关联，再长出更复杂的理论。**综合海量信息、发现模式、递归式自我改进，恰好是计算机最擅长的事。** 这里还有个容易被忽略的反直觉点。Pat Grady帮听众总结了Harmonic的模式：Lean让数学能被代码表达，形式验证提供客观的奖励函数，自我对弈驱动强化学习，迭代速度可以极快，因为环路上没有人类。Tudor认了一半。他提醒：**围棋那种完全信息零和博弈也能递归自我提升，但存在一个最优策略上限，AlphaGo再练也就那样了。数学最迷人的地方是没有上限，算力砸进去，水平一直涨。**千禧年大奖只是人类视角的里程碑，真正的问题是：它会不会停下来？他们相信它会解决比黎曼猜想难得多的、人类目前还写不出来的问题。 Vlad拿了个游戏视频打比方：有AI二十秒就通关了《我的世界》，人类玩家看了根本无法理解画面里发生了什么。未来的数学突破，大概就是这种感觉。 ## 时间表、终局，和明天就能用的三件事 节目最后是快问快答，两位创始人被迫交出了具体时间表。 - IMO夺冠：Tudor只说「很快」，追问之下Vlad给了个「也许2024」。 - 千禧年大奖：Vlad猜2029，人机混合模式可能2028。拆开看，纳维-斯托克斯方程可能2026年就有结果，黎曼猜想给到2029。Pat追问是简单的还是难的千禧年大奖，两人都笑了。 - 超越所有人类的数学推理能力：还要几年。但**未来一年内，模型在数学题上应该能到99.99百分位**，也就是一万个人里比一万个都强。他觉得陶哲轩也会同意这个判断。 Sonya补了一刀：今天的LLM连算术都经常翻车，你们这时间表够大胆的。 至于Harmonic的终局，Tudor说使命是探索人类知识的前沿，最好的情形是数学家用他们的工具关掉所有千禧年大奖难题，然后继续往前走。商业上还有软件验证：让安全关键软件被证明正确。Vlad提到，大家用Cursor和Claude 3.5已经玩出各种花活，软件工程正在从「围绕代码协作」转向「围绕规格协作」，讨论的焦点从「这段代码怎么写」移到了「我们要它做什么、怎么严格地描述它」。**当软件的成本趋近于零，被验证软件的成本也会趋近于零。往后看五到十年，新写出来的软件，大部分会是可验证、可证明正确的。**再往远处，理论物理本质上是数学，他希望能加速基础物理研究，搞清楚宇宙为什么长这样。 范围边界在哪？Vlad说公司还小，先聚焦数学和软件。但长期看，如果数学即推理这个前提成立，那理论上什么都在射程内，包括历史作文。Tudor泼了句「再看吧」。Vlad不服气，说自己数学好，历史作文也一直写得不错，亚里士多德不也写了《诗学》。 快问快答里还有个彩蛋。Vlad最崇拜冯·诺依曼：父亲是匈牙利商人，觉得数学不赚钱，找了个数学家朋友来劝退，朋友回来汇报：这人太强了，不让他搞数学是全人类的损失。后来这位劝不动的年轻人奠定了现代计算机架构，参与了曼哈顿计划，还写了博弈论的奠基之作。Tudor选了莱布尼茨：和牛顿争微积分发明权的那位，在十七世纪末提出过「普遍文字」的构想，一门演绎语言、一套自动推演程序、一座可以不断继承的知识库。**这基本就是Lean加AI的完整蓝图，比Harmonic早了三百五十年。** 听完这期，有三件事明天就能上手。 - 给AI派活时，学Lean的思路写验收标准。别只说「帮我写个方案」，把前提写清楚，把「什么叫做对了」写成可检查的输出。能被验证的任务，AI完成质量会高一截。 - 遇到难题先拆。千禧年级别的证明也是拆成小块啃下来的，一道题值不值得做，先看它能不能拆成行数更少的子问题。 - 做软件的，把「写规格」当新技能练。如果Vlad的判断兑现，几年后行业里最值钱的能力，是把需求写成机器可验证的形式，这个练习现在开始不亏。 如果只记一句话：**能被验证的东西，才能被大规模优化。**Harmonic的全部赌注都压在这半句上。想跟踪这场豪赌，盯两个先行指标：mathlib仓库的活跃度，AI在IMO级别竞赛里的成绩。至于那个43%的盘口，Metaculus上随时可以去看，甚至可以自己押一票。