AI 将如何改变数学——Harmonic 创始人 Vlad Tenev 与 Tudor Achim 谈数学超级智能
摘要
Vlad Tenev（Robinhood 创始人兼 CEO）与 Tudor Achim 联合创立了 Harmonic——一家人工智能研究实验室，其核心使命是构建数学超级智能（Mathematical Super Intelligence）。他们的核心信念是：数学即推理。与主流 AI 公司寄希望于通过规模化让数学能力自然涌现不同，Harmonic 选择直接教导模型学习数学。他们认为，精通数学的系统将在科学和工程等定量领域表现出色——正如数学能力强的学生在商业和编程等领域也能轻松迁移一样。
Harmonic 的方法论依赖三个关键要素：利用 Lean（一种形式验证编程语言）实现客观的奖励函数；通过自博弈（Self-Play）和强化学习（Reinforcement Learning）进行递归自我改进；以及生成合成数据（Synthetic Data）来训练模型。与围棋等有限博弈不同，数学没有上界——这意味着系统可以无限改进。Vlad 预测，人工智能将在近期内协助解决千禧年大奖难题，而超级智能将最终解决人类尚未构想的更难问题。
正文
数学即推理
Vlad 和 Tudor 的核心理念是：数学是所有科学和工程的基础。从黑洞到原子、从工程设计到宇宙建模，数学是人类理解世界的语言。他们认为，人类中擅长数学的人往往也擅长其他定量领域——这种迁移效应同样适用于 AI 系统。如果一个系统真正精通数学，它也会在科学和工程任务中表现出色。
与当前主流方法（如 OpenAI 和 Anthropic）依赖"规模涌现"不同，Harmonic 选择直接教授模型数学。Vlad 用自己的经历举例：在斯坦福主修数学、师从 Larry Guth 和陶哲轩（Terry Tao）后，他发现学习抽象代数和分析学让他在编程、商业合同等领域都能快速上手。"数学教会人如何逻辑思考，这种能力可以迁移到很多领域。"他认为 AI 也会遵循同样的规律。
陶哲轩、数学界与 AI
Vlad 在 UCLA 博士期间曾受教于陶哲轩——当代最伟大的数学家之一。陶哲轩的研究广度惊人：从数论、组合数学、调和分析到应用数学，甚至在 Lean 形式化证明社区也极为活跃。Vald 开玩笑道，他"偷"了陶哲轩签名的一本书，每次见面都炫耀"你拿不回去了"。
关于数学界对 AI 的态度，Vlad 认为存在代际分裂：年轻数学家普遍拥抱 AI 和形式验证工具（如 Lean），而老一辈则更为怀疑。他预测这一趋势将类似于国际象棋——最初是人类+AI 辅助阶段，但随着时间推移，AI 将变得足够强大，以至于人类的介入反而会降低结果质量。最终，"数学家"这个职业的定义将发生根本性变化，转向引导和提示 AI 系统解决问题。
为什么选择 Lean？
Lean 是一种编程语言（由 Leo de Moura 创建），最初被设计为软件验证工具，但在数学界意外获得了巨大成功。其核心思想是：数学定理的条件和结论被编码为函数的输入类型和输出类型——如果程序能够编译通过，就意味着从前提可以推导出结论。
成千上万的数学家和学生已经构建了一个名为 mathlib 的开源知识库，这是 GitHub 上最大的数学"教科书"。lean 的灵活性以及 mathlib 的增长速度远远超出预期——如今 lean 在数学领域的应用可能已经超过了在软件验证领域的应用。
对 Harmonic 来说，Lean 提供了一个客观的查错机制——系统可以验证答案是否正确，但 Lean 本身不会告诉你是否在"变得更聪明"。真正的挑战在于如何利用这些正确/错误的信号来驱动模型的快速改进。
递归自我改进与无上限进步
与围棋等有限零和博弈不同，数学的最大魅力在于——没有上界。在围棋中，系统通过自博弈改进后会达到最优策略，此后再无进步空间。但在数学中，不存在最优解：你可以不断投入计算资源，系统就会不断变得更好。
Harmonic 的系统本质上是一组智能体（Agents），它们在尝试解决数学问题。由于 Lean 可以验证答案的正误，系统能够从中提取各种训练信号来改进自身。但因为数学领域天然缺乏适用的训练数据，Harmonic 几乎完全依赖合成数据——由智能体在解题过程中自己生成。
为什么是现在？
Tudor 解释了两个关键的时间节点：首先，自回归语言模型（Autoregressive Language Models）已经变得足够强大，能够处理数学证明这种"无限动作空间"的任务——这是十年前无法想象的。其次，Lean 经过了长足发展，Lean 4 在 2023 年 9 月才正式发布，mathlib 的壮大让 AI 系统有了可以构建的知识基础。
"如果你在 20 年前告诉数学家，形式化方法将成为数学界的主流关注点，他们会觉得你疯了。"但如今，AI 系统的成熟与 Lean 的成功正在汇合，使得攻克数学超级智能的时机真正到来。
AI 将赢得千禧年大奖吗？
Vlad 提到，在 Metaculus 预测平台上，下一个千禧年大奖难题由 AI 解决的的概率为 43%。而他本人认为这是低估的。"如果人类能在很近期内解决黎曼假设，那会很了不起——但再下下个问题，几乎肯定会由 AI 大量参与来解决。"
Harmonic 的目标不仅是解决黎曼假设或赢得千禧年大奖——那些只是"人类的里程碑"。真正的远景是：系统将解决远比黎曼假设更困难的问题，那些我们甚至还没有能力去构想的问题。