三家 IMO 金牌都错第 6 题，Harmonic 想用 Lean 把数学变成可执行文件

2025 年国际数学奥林匹克，三家 AI 实验室宣布拿到金牌水平成绩：OpenAI、Google DeepMind，以及名气小得多的 Harmonic。三家都做错了同一道题，第 6 题。Vlad Tenev 在播客里说，这道题对人类也大约难 5 倍，步骤多，还需要一种目前很难形式化编码的空间推理。

Harmonic 是 Vlad Tenev 和 Tudor Achim 联合创办的 AI 研究实验室，产品叫 Aristotle。Vlad 更广为人知的身份是 Robinhood 的联合创始人兼 CEO，斯坦福数学博士项目出身，后来退学去创业。Tudor 是 Harmonic 的 CEO，斯坦福博士，做过自动驾驶创业。两个人的共同点是都相信一件事：数学就是推理，而推理可以被机器检查。

这期播客里，Nathan Labenz 和他们聊了两个小时，从形而上学一路聊到 2030 年的科学图景。中间穿插了大量关于 Lean、MathLib、蒙特卡洛树搜索的技术细节，也有一段我听完之后愣了几秒的愿景。

数学就是推理，其余都是副产品

Tudor 给数学下的定义很朴素：数学是人类把理解拆成一连串别人能检查的逻辑步骤的过程。解物理题、报税、想宇宙起源，最后都得有一个自洽的解释，能从其他事实推出来，同事能验证。

这个定义把数学从电影里那种天才在黑板上写神秘符号的场景里拉了出来。Vlad 补了一段自己的经历：他进斯坦福本来想学物理，读布莱恩·格林的《宇宙的琴弦》，小时候第一本从头读到尾的英文书是霍金的《时间简史》。他想搞明白大爆炸之前发生了什么，为什么会有引力、电磁力、强核力、弱核力这么多种力，是不是本来只有一种，随着宇宙冷却膨胀才分裂开。结果每次问到深处，物理系都把他送到数学系：想懂弦论，先懂微分几何；想懂广义相对论，先懂微分几何。他就这样成了纯数学博士。

Tudor 引了物理学家 Eugene Wigner 那篇著名文章《数学不合理的有效性》。爱因斯坦搞狭义相对论的时候，用上了 19 世纪数学家关于流形的思想实验。那些思想实验在当时看几乎荒唐，没人觉得能用在真实的三维世界里。结果它们恰好能描述加进时间与曲率之后的四维世界。数论也一样，被当成最没用的分支养了很多年，后来成了整个数字加密经济的基础。

Tudor 的结论是：别问数学有什么用，先做，总有一部分会比你想象的更有用。投资数学不只是为了造一个更聪明的系统，也是为了生产出大量新数学，以后再想办法用。

Lean 是什么：三个公理撑起全部数学

Lean 是这期节目里出现频率最高的词。Tudor 说它是有史以来最好的编程语言，理由是你能在 Lean 里写 Python、C、C++ 能写的任何程序，同时还能表达几乎任何逻辑概念。它是依赖类型语言，编译时就能检查程序的各种复杂性质。光谱的一端是 JavaScript，几乎什么都检查不了；另一端是 Lean。

Nathan 问了一个很实在的问题：这个空间到底有多大？有多少符号、多少公理、多少规则？

Tudor 的回答是：Lean 证明依赖三个公理。其中两个极其技术性，一个叫命题外延性，一个和商类型的可靠性有关。第三个是选择公理，意思是如果你有一个非空集合，你就能从里面挑一个元素。这句话听上去像常识，历史上却引发过激烈争论。三个公理加起来，每个的数学表述都不超过一条推文的长度，选择公理在 Lean 里的定义大概只有 10 个字符。从这三条出发，你能建起全部数学、计算机科学、物理建模、经济学、统计学、生物学。

Nathan 要一个类比，Tudor 给了国际象棋。一个定理相当于“从棋盘的这个初始摆法，能走到那个目标摆法”，一个证明相当于列出每一步走法，Lean 的内核逐条检查：这一步在规则手册里吗。检查通过，定理成立。内核本身很小，被很多人反复审过。MathLib 则是建在内核之上的巨大仓库，Tudor 形容它是全世界每一本数学教材合并成一本，而且自洽。你可以在里面搜任何概念，点“跳到定义”，一路跳下去。

Vlad 补了一个细节：Lean 4 发布和 GPT-4 发布几乎同一个月，也是 Harmonic 成立的那个月。两件事同时成熟到这个程度，才有了把形式化工具和 AI 拼起来的可能。

Aristotle 的三个零件，以及为什么幻觉是特性

Aristotle 拿 IMO 金牌时的架构有三个部分。

第一部分是蒙特卡洛树搜索，Nathan 把它类比成 AlphaGo：系统在可能的推理路径上试探，有一个学习出来的评分函数判断这条分支看起来有没有希望，然后往深处搜。Tudor 纠正了一点：这个搜索本身在做大量高层推理，不靠简单蛮力。它处理的“引理”更接近“解一道有难度的数学题”，而非“证明 2 的平方等于 4”。只有搜到足够低的位置、开始关闭子案例的时候，才更像磨。

第二部分是引理猜测模块，技术报告里叫非形式推理系统。Nathan 把它理解成“给我一座大山，先猜几个大本营在哪”。Tudor 认可这个比喻，同时加了一句关键的话：这个系统本身会犯海量错误，不能把它想成一个聪明人在地图上标出路线，它更像一个能提出大量错误想法的系统，你从里面拼出能用的东西。它的作用之一是上下文管理：处理小步骤的时候，不必记住大步骤的全部上下文。

第三部分是几何模块，模仿 DeepMind 的 AlphaGeometry。Vlad 解释了为什么几何先被攻下：几何受约束，三个点之间角度就那么多，点到 10 个、15 个会爆炸，但那时候人也难解了。Tudor 说几何模块才是真正的磨，它枚举几何图形的所有可能结论，模式识别智能不多。

Nathan 还试了 Aristotle 的非形式模式，让它证明“爱即一切”，系统回答这是哲学陈述，超出 Lean 4 内核的能力范围。他又让它证明“爱泼斯坦没有自杀”，系统回答这是时事陈述，同样超出范围。Vlad 说第一版 Aristotle 其实会给“爱即一切”建一套理论然后给出一个证明，他们后来在产品上收窄了范围，目的是让用户尽快发现这东西真正擅长什么。他还提到自己问过一个天文问题：帕洛阿尔托 50 英里内下一次日全食是什么时候。现有模型经常答不好，因为网上没人问过一模一样的问题，得从第一性原理算。

Tudor 对幻觉的看法值得单独拎出来。他说幻觉是推理系统的关键部分，是模型探索人类从未编码过的东西的途径。Aristotle 在 IMO 上犯了很多错，试了很多走不通的路径，正是这种探索让它最终找到正确答案。追求完全无幻觉的 LLM 这个想法本身不太成立，当然要配上 Aristotle 这样的端到端验证系统。Vlad 补了一句：人类也一样，最有创造力的人往往也是幻觉最多的人。

同行评审的终结，品味交给社区

Vlad 讲了一段数学界正在发生的变化。他读博士的 2000 年代末，做数学几乎不用电脑，思考在黑板上，合作在办公室黑板或者会议上。Lean 把数学从黑板搬进了 VS Code 和 Cursor，证明放上 GitHub，可以几十人协作。就算把 AI 拿掉，Lean 本身已经改变了数学的工作方式。现在有知名数学家组织大型项目，几十人一起形式化费马大定理的证明。

更深的冲击在信任机制上。以前一个数学家证明了一个东西，得有人花时间读，读完说对不对。费马大定理的“证明”是一群人聚在一起，大家都同意证完了，它就被追认为证明。Lean 让这一步变得不必要：证明通过检查，就不需要人工验证，前提是 Lean 内核和你陈述问题的方式没有 bug。

Tudor 拿开源软件做类比。GitHub 上开一个 pull request，测试过了、作者认可风格，就合并，不需要谁认识你。影响力用 star 数、fork 数、依赖图来衡量，守门人消失了。数学会走同一条路：大项目里任何人贡献证明，Lean 接受就成立，被很多人依赖的结果会积累起 fork 和 star。从大教堂式开发走向集市式开发，Lean 是那张计算证书。

Vlad 给了一个时间尺度的论证：假设五年后 AI 自主产出的证明从 5 到 10 页变成 5000 页，谁去读？没人读 5000 页的数学证明。验证时间不能随证明复杂度线性增长，所以未来一定是形式化的。Tudor 说这正是 Harmonic 2023 年成立时的思想实验：如果十年后让模型证明黎曼猜想，任何模型都会给你输出 10 万页，你只能扔进垃圾桶，一是里面大概有错，二是你根本处理不了。两个假设都被验证了：形式化输出让人类可消化、提供高确定性；形式化也带来了更高效的强化学习方式。跟大实验室比，Harmonic 的资源少得多，在 IMO 上却打出了超出量级的成绩。

问题选择的品味，Harmonic 做了一个明确的决定。IMO 金牌之后有两条路：把系统关起门来，招一批数学家秘密做问题，定期宣布 Aristotle 又做完了 X、Y、Z；或者开放 API，让社区用 API 额度投票决定做什么数学。他们选了第二条。不说 Navier-Stokes 比 P vs NP 更重要，让数学家用调用量说话。结果他们看到大量对计算机科学、密码学、某些数论分支的兴趣，有一阵子图论猜想特别多。Vlad 说这背后是一个世界观问题：未来是几个两吉瓦数据中心的大实验室包揽所有发现、拿走所有价值，还是几百万人拿着工具各自工作、互相协作、自己拿到功劳。他赌第二种。

训练的时候有没有数学家小组给证明的优雅度打分？Tudor 说两年里他们做过零次这种事。他们优化的指标是未来证明的计算成本净现值。这个指标天然防住一种现象：强化学习早期解简单题可以靠蛮力磨过去，但磨出来的习惯会在后面害你。两个都不靠磨的证明，一个明显更长更低效，就选短的。他们信奉 Bitter Lesson，尽量少给系统先验，让强化学习在规模上跑。

社区实际在做什么？有人在验证密码学实现，问有没有可能两个不同输入给出同一个输出，从而违反这个算法的某个原则；有人在验证自动驾驶控制器，问存不存在一串输入会让系统进入不稳定死区。Tudor 说这些逻辑推理和数学推理是同一种东西。

2030 年的理论丰裕，与一个受约束的输出空间

Nathan 问 2030 年这个系统在干什么，Tudor 的回答让节目安静了一下。

他的判断是：到 2030 年，我们基本上会对一切都有理论解释。科学史上有智力跃迁和数据跃迁两种时刻。显微镜出现，生物学理论爆发；电子显微镜出现，化学理论爆发。现在真正的瓶颈是能进行最高水平逻辑推理的人太少，统一广义相对论和量子力学太难。任何能被数学表述的东西，底层都是科学，我们会拿到自洽、说得通的理论。然后重新进入数据受限的阶段：可能会有五个统一量子力学和广义相对论的理论，都解释现有数据，得造更高能的实验去分辨谁对。造对撞机要等。

Nathan 确认了一遍：你的意思是，会有多个大统一理论都符合现有数据，然后靠对撞机实验来裁决哪个是真的。Tudor 说是，AI 不是全知的，能推理的是能扎根在自己逻辑推导规则里的东西，宇宙有些部分你必须做实验才知道。他补了一句，在到达那一步之前，效用已经很大了，这只是渐近终点。

聊到最后，Nathan 把话题拉到安全。他提到 Eliezer Yudkowsky 说过，真正的超级智能看一张静态图片就能推导出全部物理，同时也认为这东西极其危险。Vlad 的回答是：目前不太担心，因为系统输出受约束。Aristotle 不会去调你的 Gmail 或 iMessage API，它往外输出的就是 Lean 文件。第一批危险大概会长成网络安全事件的样子，模型自主调 API、和别的系统交互，既制造 API 层的漏洞，也提供利用漏洞的机制。等 Harmonic 真把模型接到外部世界、接口不再是 Lean 文件的时候，就得认真对待。

Tudor 补了可解释性的角度。很多人研究可解释性，是为了信任。Harmonic 一开始就做了明确选择：输出形式化验证过的推理，这本身就是最大程度的可解释性。计算机能检查，人想理解就一路点“跳到定义”，像浏览代码库。至于模型内部怎么做到这么聪明，他们以后会好奇、会研究，但信任问题在输出层已经解决了。

Vlad 最后说了一段公司价值观层面的话：他们相信人类应该站在这一切进步的中心，人类加速它，但人类掌舵、做决定。这也是为什么他们要把工具放到几百万人手里，而不是做一个关起门来发大新闻的实验室。

明天就能做的几件事

第一，去玩 Lean 的 Natural Number Game。Vlad 在节目里推荐的，用三个公理和 Lean 语言证明加法交换律、分配律这些基本事实，不需要任何研究数学背景。想再难一点，有 Real Analysis Game，从序列、实数、集合大小开始，一路证到微积分基础。

第二，注册 Aristotle 的免费账号，拿一个你自己工作里的逻辑问题去试。别让它算 2+2，那个 MathLib 里早证过了。试一个你写过的代码里的边界条件问题：这个循环在什么输入范围下会让输出越界？这个加密实现有没有可能两个输入撞同一个输出？

第三，留意形式化验证在关键系统里的扩散节奏。密码学、自动驾驶控制器、航空航天，这些领域已经在用 Lean、Rocq、Isabelle，只是方式很手工，雇专家一点点形式化。AI 会先加速这批人的工作，然后往普通软件扩散。如果你的团队在写任何出错代价很高的代码，这是未来两三年值得提前押注的方向。

第四，如果你关心 AI 安全，Vlad 那句“约束输出空间”值得记下来。一个系统能对外部世界做的事越少，你能信任它的理由就越多。这比事后解释模型内部在想什么，要朴素得多，也可行得多。

节目的最后，Nathan 说他既受启发又有点害怕。我听完的感受差不多。一个能在 2030 年给一切可数学化现象提供自洽解释的系统，同时把验证成本压到接近零，这个组合的威力比再拿一块 IMO 金牌大得多。真正改变游戏规则的，是验证这件事本身从零变成了可规模化的一。