为什么 Harmonic 的 Vlad Tenev 和 Tudor Achim 认为 AI 即将改变数学——及其重要性

coverSequoia Capital · 2024-09-24🎬 在 YouTube 观看原视频 →>

摘要

Robinhood 创始人兼 CEO Vlad Tenev 与 Tudor Achim 联合创立了 Harmonic——一家致力于推动人类知识前沿的 AI 研究实验室。Harmonic 的核心论点是：数学即推理（Math is Reasoning），理解数学是理解并推理广阔世界的最佳路径。这与主流基础模型公司"让数学作为规模化副产品涌现"的策略形成鲜明对比。

Vlad 的数学背景令人瞩目：斯坦福数学专业，曾师从当代最伟大的数学家之一陶哲轩（Terence Tao）。他用自己的经历论证了数学能力向其他领域迁移的现实性——从抽象代数到创业、编程、商业谈判，底层的逻辑推理能力一以贯之。

Harmonic 的技术路线具有独特的结构性优势：利用精益语言（Lean）实现数学的代码化和形式化验证，从而获得客观的奖励函数（Reward Function）；通过自博弈（Self-Play）和强化学习实现递归自改进（Recursive Self-Improvement）；合成数据（Synthetic Data）成为模型训练的主要燃料，突破了互联网数据的"数据墙"限制。与棋类游戏不同，数学没有上界——投入越多算力，模型就会持续提升，永无止境。

Vlad 预测，AI 辅助人类解决千禧年大奖问题（Millennium Prize）的时间表为 2028 年（混合模式），黎曼猜想（Riemann Hypothesis）有望在 2029 年被 AI 攻克。更远期来看，验证软件（Verified Software）将成为常态，软件工程的重心将从代码审查转向规格协作。

正文

数学即推理：Harmonic 的核心理念

Tudor Achim 开宗明义地阐述了 Harmonic 的创始信念："如果你环顾所有科学与工程领域，数学几乎是它们共同的基础。数学已经成为人类理解宇宙的方式——从黑洞到原子，从工程设计到自然现象建模，数学是底层语言。"

数学之所以独特，在于两方面的属性：首先，宇宙恰好可以用数学来解释——你可以用一组紧凑的符号来描述现象；其次，数学是一种构建共享认知理论的方式，它客观、清晰、透明。当两个人讨论一个严谨的话题时，可以写下一组演绎规则，就基本前提达成一致，然后推导出结论。

Vlad Tenev 用自己的经历为这一论点提供了生动注脚。从童年起他就展现出数学天赋，在斯坦福主修数学，之后进入 UCLA 攻读数学博士（虽然只完成了一年便"辍学"创业）。"我刻意不关注其他任何东西——可能只上了一门斯坦福的计算机编程入门课。五年后当我成为创业者时，我发现学编程异常容易，理解合同也很轻松。"他强调，抽象代数和分析的逻辑基础远比商业合同复杂得多。

Harmonic 的核心假设是：如果你让一个 AI 系统真正精通数学，它将展现出与人类相似的迁移效应——在科学和工程领域表现卓越，即便它不会立刻写出世界顶尖的历史论文。

与陶哲轩的师生缘

Vlad 在 UCLA 的第一年有幸师从陶哲轩学习研究生级别分析课程，这段经历至今令他难忘。"陶哲轩的过人之处在于其研究广度——大多数数学家只在一个狭窄领域深入，而他能在数论、组合学、调和分析、应用数学等数十个领域都做出贡献。"

Vlad 还分享了一个有趣的轶事：陶哲轩曾借给他一本书并在上面签名——"我认为他签名是为了确保我能还给他。但他不知道，这一签名让我永远不会还了。每次见面我都告诉他：'那本书你别想要回来了，它现在就放在我书架上，和我的其他签名首版书在一起。'"

谈到数学界对 AI 的态度，Vlad 观察到代际分化：年轻数学家普遍支持 AI 和形式化验证工具（如 Lean），而老一辈则相对怀疑。"这不奇怪，几乎每个领域都一样。"他预测数学的发展轨迹将类似于国际象棋——先经历漫长的"人类+AI 辅助"阶段，然后 AI 逐步占据主导。

Lean：形式化验证的关键基础设施

Tudor 详细解释了 Lean 在 Harmonic 技术栈中的核心角色。Lean 是一种编程语言，由 Leonardo de Moura 创建（现任职于 Amazon AWS）。其精妙之处在于：数学命题被编码在语言的类型系统（Type System）中——函数的输入类型对应定理的前提假设，输出类型对应结论。"如果函数编译通过，就意味着你可以从输入类型推导出输出类型，进而证明你可以从前提推出结论。"

有趣的是，de Moura 最初开发 Lean 的目标是软件验证工具，而非数学应用。"他希望创建更好的软件验证工具，这一目标本身非常崇高。但他没有预料到的是，软件验证的本质就是证明软件具有某些属性——这让 Lean 在数学界爆红。"

如今，成千上万的数学家和学生共同构建了一个名为 Mathlib 的开源数学知识库，可以被视为"GitHub 上最大的数学教科书"。Vlad 认为，Lean 在数学领域的应用可能已经超过了其在验证软件方面的使用。

为什么是现在？两个关键变量

Harmonic 选择这个时间点切入 AI 数学领域，基于两个关键判断：

第一，自回归语言模型已经足够强大。Tudor 回忆道，早在 2015-2016 年他就与朋友讨论过用强化学习做定理证明的问题，但当时的瓶颈在于：围棋等游戏中，动作空间是有限的（落子位置），而在数学中，下一步可以是任何内容——你需要一个能在无限动作空间中做出预测的系统。如今，自回归语言模型已经具备了这种能力。

第二，Lean 已经足够成熟。"如果你在 20 年前告诉一位数学家，形式化方法将引起整个领域的广泛兴趣，他们可能会觉得你疯了。"Lean 4 在 2023 年 9 月才正式发布，其灵活性和社区的快速增长使形式化数学从边缘走向主流。

合成数据与递归自改进

Harmonic 的核心训练范式中，合成数据（Synthetic Data）扮演着关键角色。Vlad 解释说："与大多数 AI 领域相比，数学是一个数据贫乏（Data Poor）的领域。互联网上数学数据的规模远不及猫咪视频。"Mathlib 虽然是一个宝贵资源，但它以通用和紧凑的方式编写，并不直接适用于问题求解。

因此，Harmonic 的训练过程本质上是"智能体自身在不断尝试解决问题的过程中生成训练信号"。系统从简单问题开始，逐步递归提升，就像人类从基础公理出发构建复杂数学结构一样——"费马大定理的证明长达 200 页，非常复杂，但最终是通过将问题分解为更小模块来解决的。"

Vlad 指出，这恰好解决了当前基础模型公司面临的"数据墙"困境。"如果你依赖猫视频和维基百科内容训练模型，如何能获得远超这些数据质量的智能是一个开放问题。你必须进入某种自我强化、自博弈的机制，才能超越人类数学家和研究者的能力。"

无限的上界：数学没有终点

与围棋等零和博弈不同，数学的递归自改进没有理论上界。Tudor 解释道："围棋中你通过自博弈不断提升，但最终会触及最优策略（Optimal Strategy），在那之后无论投入多少算力都不会有进一步提升。数学最令人兴奋的地方在于：没有上界。你持续投入算力，它就持续变得更强，永无止境。"

这意味着人类定义的里程碑——如解决黎曼猜想或赢得千禧年大奖——只是沿途的站点，而非终点。Tudor 用 Minecraft 的比喻来形容这一前景："你看过 AI 在 20 秒内通关 Minecraft 的视频吗？就像那样——人类甚至无法理解它是怎么做到的。我认为我们在数学领域将解决许多比黎曼猜想更难的、我们尚未构想出来的问题。"

在时间表方面，Harmonic 团队给出了大胆的预测：2025 年（或更早）赢得国际数学奥林匹克（IMO）；2028 年 AI-人类混合模式攻克千禧年难题；2029 年解决黎曼猜想；在推理能力方面，一年内达到 99.99 百分位水平，几年内达到甚至超越陶哲轩级别的超人类水平。

从数学到验证软件：更广阔的应用前景

Harmonic 的长期愿景远不止于纯数学。Vlad 展望了验证软件（Verified Software）的未来："随着软件编写的成本趋近于零，验证软件的成本也将趋近于零。这个曾经不切实际、需要专业人类工程师投入大量精力的领域，将通过 AI 实现戏剧性加速。"

他预测，5 到 10 年后，"绝大多数编写的软件都将是经过验证且可证明正确的"。软件工程的工作重心将从"审查代码"转向"协作定义规格"——"我们想要代码做什么？我们能否对此更加严谨？"

Tudor 补充了理论物理方面的潜力："理论物理本质上是数学，是前沿数学被应用的主要途径之一。能够加速基础物理前沿的研究、真正理解宇宙为何如此、物理定律为何存在——如果我们为此做出贡献，我将感到无比自豪。"

快速问答