数学超级智能：Harmonic 的 Vlad 与 Tudor 谈 IMO 金牌与万物理论
摘要
Harmonic 的核心押注是：数学就是推理，而经过形式化验证的输出，能把 AI 能力变成用户可以信任的东西。 Aristotle 生成带注释的 Lean 代码，其每一步都由小型内核依据3条基本公理检查，但前提是内核和定理陈述本身设置正确。产品目标是打造一台“惊人的计算器”：拥有前沿模型的表达能力，同时具备计算器般的可靠性。
Aristotle 在2025年 IMO 达到金牌水平，支持了 Harmonic 关于强化学习可以围绕可验证奖励实现异常高效扩展的判断。 Harmonic、OpenAI 和 Google DeepMind 都未解出第6题；Achim 估计，即便对人类而言，这道题可能也难5倍，而且异常依赖空间推理，但 Harmonic 在继续运行中看到了“生命迹象”。创始人预计能力将大致平滑地呈指数增长，并称相较于规模更大的实验室，Harmonic 已经“远超自身体量出拳”。
Lean 4 和 Mathlib 可能以计算认证和开源分发，替代数学同行评审中相当大的一部分工作。 Mathlib 被描述为“以自洽方式合并成一个整体的全世界每一本数学教材”，而 Lean 允许贡献者通过类似 GitHub 的工作流提交证明，正确性靠测试验证，而不是靠社会声望背书。数学声望可能从期刊把关人转向 stars、forks、依赖关系和复用率，让精英机构之外的贡献者也能参与严肃数学。
形式化验证可能成为 AI 生成软件的控制层，首先从错误代价最高的领域开始。 创始人介绍称，API 用户正在检查密码学实现是否具备碰撞性质，并考虑自动驾驶控制器是否存在导致系统不稳定的输入序列；他们还表示，用户已经在用 Aristotle 检查安全关键软件。更长期看，创始人质疑 AI 为什么还要编写 Python 或 Java——这些语言主要针对人类可读性进行了优化。如果智能体能生成约150万行的浏览器或5000页的证明，人工审查就无法继续扩展，由此可能从手工形式化方法走向“形式化氛围编程”。
Harmonic 正把开放访问同时作为分发策略和数学品味的去中心化机制。 Harmonic 不雇用内部团队来决定 Navier–Stokes 是否比 P versus NP 更重要，而是通过 API 和网页界面开放 Aristotle，让社区需求来分配算力。创始人更偏好一个由数百万获得工具赋能的研究者组成的未来，而不是“一个拥有2吉瓦数据中心的巨型 AI 实验室”垄断每项发现及其价值。
其训练理念偏向可扩展的搜索，而不是依赖人类对美感的监督，同时把幻觉视为必要的探索机制。 Harmonic 几乎没有做过数学家小组参与的优雅证明 A/B 测试；相反，研究人员优化 Achim 所说的“未来证明的净现值”，惩罚那些能靠蛮力解决简单任务、却无法建立可复用能力的方法。预训练模型仍然是有用的起点，也可能与更高熵、较少受人类方法束缚的系统结合：“幻觉让模型能够探索此前从未被人类编码过的东西。”
2030年的愿景不是立即获得全知，而是理论上的丰饶，随后迎来新的数据瓶颈。 Achim 想象，也许会出现5套内部自洽、统一量子力学与广义相对论的理论，科学家需要越来越高能的实验来区分它们——这是“基本上能够解释一切的理论”，但不是无需观测就拥有知识。Harmonic 当前仅允许 Lean 文件作为行动空间，因此运营风险有限；创始人预计，一旦这类系统获得 API 和自主性，网络安全风险会升高，并坚持“人类应该掌舵并作出决定”。
精读
1. 数学就是推理，而抽象的效用往往姗姗来迟
Achim 对数学的核心定义不止于定理证明：“数学就是推理”，也就是把一个解释拆解成“由一连串微小逻辑步骤组成”的过程，让其他人能够逐步检查。物理学、税务、宇宙学和工程学的研究对象不同，但最终都需要一套从明确事实出发、内部自洽的解释。
Achim 是通过物理学进入数学的：先读 Stephen Hawking 和 Brian Greene，之后进入 Stanford。关于大爆炸、引力，以及今天的各种力是否都从“起初的同一个东西”中分化出来的问题，反复把他从物理学引向微分几何和纯数学；他的实际链条是数学通往物理，物理通往工程，工程最终通往飞行器、晶体管、GPS 及其他有价值的系统。
“数学非理性的有效性”构成了 Harmonic 对“数学必须立即产生效用”这一要求的回答。关于流形的抽象研究后来成为相对论的关键，数论也从一项深奥的学术追求变成安全数字经济的基础。因此 Achim 的建议带有投资组合思维：“你只管做数学”，因为其中一部分最终会比任何人最初设想的更有用。
创造一个重大新思想的数学家极其罕见，往往5到10年才有一次；另一类则是高产的综合者，他们吸收论文、记住技术，并把方法迁移到不同领域。AI 未来或许能加速前一类人的工作，但 GPT-4 已经显示出对后一类人的杠杆效应：搜索庞大的文献，找回相关技巧，再以任何个人读者都无法匹敌的速度组合知识。
2. Lean 把证明变成可执行的证书
Achim 称 Lean 是“有史以来最好的编程语言”，因为它同时覆盖普通程序和逻辑命题。作为依赖类型语言，Lean 能在编译阶段表达复杂性质，而不是仅仅运行代码后再检查结果；在他的光谱中，JavaScript 几乎不检查任何东西，而 Lean 可以在执行前指定并验证异常丰富的不变量。
Lean 建立在构造演算和3条公理之上：命题外延性、公理化商集的可靠性，以及选择公理。最后一条公理表示可以从非空集合中选出一个元素；3条公理都短到一条推文足以容纳。创始人认为，这个极简基础足以支撑数学、计算机科学，以及物理、经济学、统计学和生物学中的定量建模。
Nathan Labenz 的国际象棋类比依然成立：一个定理说明棋盘可以从起始局面走到目标局面，而证明则列出中间的每一步。Lean 的内核依据规则手册检查每个声称的步骤，并验证最终状态确实已经到达。这里的步骤不是棋步，但证书具有同样的结构：不断重复“这一步是正确的”，直到抵达终点。
学习曲线可以从研究数学以下的层级开始。Achim 推荐 Natural Number Game，用户可以在那里推导加法和乘法的性质；他还提到一款实分析游戏，内容从数列和实数逐步推进到微积分基础。他更大的判断是，数学教育将从黑板迁移到计算机实验室，甚至可能触及中学生。
3. Mathlib 可能把数学从期刊带到 GitHub
Tenev 记得自己在2000年代末做数学时，几乎完全依赖黑板、白板和沙发，电脑主要用于把完成的成果排版。Lean 把工作过程迁移到 VS Code、Cursor 和 GitHub，使地理上分散的协作成为可能：几十个人可以共同形式化研究，或者一起攻克费马大定理这样的项目。
Mathlib 在 Lean 的小型内核之上提供可复用的高层次操作。它覆盖代数、几何、实分析、统计学等领域，把定义和已经证明的结果整合起来，调用方式类似软件库中的函数。Achim 所设想的终点是“以自洽方式合并成一个整体的全世界每一本数学教材”，并且可以在普通电脑上从基础重新构建。
形式化改变了信任机制，但有两项前提必须保留：Lean 内核必须没有漏洞，定理也必须忠实表达原本想表达的命题。在这两个条件成立时，经过检查的证明不再需要一位有声望的数学家为每一步背书。“公民数学家”可以直接贡献一份证书，而不必说服精英院系或期刊来证明其正确性。
Achim 把这一转变类比为开源软件从“大教堂”走向“集市”。任何人都可以提交证明；Lean 负责测试正确性，维护者可以评判风格，而 stars、forks、依赖关系和复用率则可以衡量影响力。时间点同样关键：Lean 3 仍然像测试版软件，Lean 4 和 GPT-4 则在 Harmonic 2023年成立前后变得真正可用。
4. Aristotle 在多个尺度上搜索，而不只是蛮力穷举
Labenz 将 IMO 时代的系统拆解为蒙特卡洛树搜索、非正式引理生成器和几何专家，但 Achim 修正了“树搜索只是蛮力”的理解。语言模型会推断具有决定性意义的高层步骤，并解决困难的子问题；只有深入搜索树后，工作才会变成例行的分类收尾。
搜索机制本身由 LLM 构成：一个组件提出步骤，另一个组件为步骤打分，二者围绕引理协作，最终拼装出完整的 Lean 证明。非正式推理器更适合理解为上下文管理器，而不是永远正确的登山向导。它会产生“数量巨大的错误”，包括错误的方案，或根本无法形式化的方案，但有用的中间落点仍可能从中浮现。
几何模块更接近真正的“磨床”。Labenz 把它比作 AlphaGeometry；Achim 说，它先探索高层步骤，再用算法把后果逐一磨出来。几何较早被解决，部分原因是其对象和关系受到约束——点只能产生有限数量的角度；但当图中出现10个或15个点时，搜索空间仍会迅速爆炸。
另外两个不太显眼的组件承载着相当大的产品价值。自动形式化负责把自然语言提示忠实翻译成 Lean；理论构建则创造 Mathlib 中尚不存在的结构，并在证明搜索过程中将其纳入。Achim 提醒，IMO 系统之后，架构已经经历大幅整合和修改；技术报告描述的是一个不断变化的截面，而不是固定不变的产品。
5. 当人们无法就有效推理达成共识，可证性就到此为止
Labenz 用刻意别扭的提示测试非正式模式。让 Aristotle 证明“万物皆爱”，它把命题归为哲学问题，认为超出 Lean 4 的范围；让它证明“Epstein 没有自杀”，它则把该陈述当作时事问题，而不是形式化定理。这些拒答暴露出证明之前更困难的一步：判断一个混乱的现实世界陈述究竟应当被忠实表达成什么命题。
Achim 认为，最终边界会落在“人们能够就何种推理序列算作有效达成共识”的地方。数学和国际象棋天然符合；定量软件行为也符合，因为输入、分支、循环和输出之间存在可检查的关系。他不太相信历史论文能够变得客观可验证，暂时把目标限定为“任何本质上属于定量和逻辑的东西”。
现有 API 的使用说明了软件领域的延伸。一段密码学实现可以被检查两个输入是否可能发生碰撞，尤其是在算法要求唯一性的情况下；自动驾驶控制器也可以通过符号方法测试是否存在会制造不稳定死区的输入序列。单元测试是在代码存在之后抽样执行，而形式化推理则可以尝试证明：对于满足既定假设的全部输入，系统都会表现出某种行为。
Tenev 在创始人的分歧中站得更开放一侧。早期 Aristotle 或许可以围绕“万物皆爱”发明一套理论，而用户已经提交了生物学、医学、经济学和金融数学问题；当前限制主要是把客户引向可靠价值。他可以想象，把互联网事实明确写成公理；而天文学问题——例如 Palo Alto 50英里范围内下一次日全食何时发生——已经显示出，第一性原理计算为何胜过信息检索。
6. 数学品味来自社区需求，而非内部评审小组
在 Aristotle 达到 IMO 金牌水平后，Harmonic 面临一个选择：把系统留在内部，招募顶尖数学家，定期宣布私下完成的成果；还是把它广泛开放。公司选择了 API、终端界面，随后又推出网页界面，让社区的“显 revealed preference”决定哪些问题值得投入算力，而不是由公司宣布 Navier–Stokes 比 P versus NP 更重要。
这一选择暴露出 Harmonic 内部不会优先处理的工作，包括计算学习理论、图论猜想、计算机科学、密码学和数论的若干分支。Tenev 把战略分叉说得很直接：发现可以从一个捕获全部价值的2吉瓦实验室中产生，也可以来自数百万拥有工具、独立工作、彼此协作、获得署名并保留更多上行收益的人。
Labenz 追问的是另一种品味：Aristotle 的证明是否优雅，而不只是正确。Harmonic 几乎没有通过数学家小组进行证明 A/B 测试。Achim 则把目标描述为“未来证明的净现值”——偏好那些能降低未来解决日益困难问题的计算成本的方法，而不是只追求今天让人类评审者印象深刻的证明。
这个目标内含一种刻意保留的张力。蛮力可能在简单问题上高效地产生短期答案，却什么可复用的东西也没有教会系统，未来反而变得昂贵；对于真正经过推理的解法，则偏好更短、更高效的证明。Harmonic 遵循“苦涩教训”：有用时从预训练模型出发，施加尽可能少的先验，扩大强化学习规模，并可能混入更高熵、较少受既有人类数学偏见影响的系统。
7. 可验证输出取代对模型内部的理解
Labenz 追问，可解释性是否能揭示数学模型内部的新抽象，或者 Aristotle 最终是否会与一个更模糊的世界模型合并——他戏谑式的终点是，由一个仁慈的“安全 HAL 9000”驾驶宇宙飞船。背后的担忧是，正确性证书或许只能告诉我们模型证明了什么，却不能解释其内部表征如何生成这一洞见。
Achim 回应说，人们往往把可解释性当作可信度的代理指标，而 Harmonic 在公司成立初期就通过要求形式化输出解决了这个问题。Lean 是“最具可解释性的输出”：机器可以检查它，人类则可以反复使用“转到定义”，像浏览代码库一样遍历整个证明。模型在机制层面或许仍然不透明，但其会对外产生后果的推理是可检查、可认证的。
因此，Harmonic 优先追求廉价、经过验证的证明，而不是打开神经网络的黑箱。一位创始人提出——同时承认“我可能错了”——更容易理解的路径也许是研究 Aristotle 如何把3个数学子领域的技术组合成一份前所未有的解答。这种行为层面的解释，可能比挖掘权重、寻找他们尚未观察到的内部“超级智能火花”更有用。
8. IMO 金牌与从非正式到形式化的阶段跃迁同时发生
Harmonic、OpenAI 和 Google DeepMind 都在2025年 IMO 达到金牌水平，也都未解出第6题。Achim 估计，这道题即便对人类而言也可能难5倍，其中包含许多步骤和难以形式化的空间推理。继续运行后出现了“生命迹象”，因此他认为最终解出这道题是可能的，而不是把它视为架构遇到的天花板。
第3题和第5题很可能在仅仅一年前还会超过大多数模型的能力，这强化了创始人对能力大致平滑指数增长的判断。社区工作流也开始呈现组合性：Labenz 看到 GPT-5.2 Pro 在 token 空间生成候选证明，随后由 Aristotle 将其形式化并检查。与此同时，Aristotle 用户已经解决了一些曾经开放了30年或40年的中等难度问题。
Achim 认为真正的断点发生在别处：“向形式化跃迁的阶段转变”已经发生。数学家不久前还会觉得可笑的工作——上传一篇完整的数论论文，自动将其翻译成 Lean——如今通过多次运行 Aristotle 已经可以实现。Harmonic 甚至考虑过一个“Ralph 按钮”，只要按下就让系统持续运行直到形式化完成，让人类负责选择问题、评估技术，而不必检查每一个推导。
规模让创始人对终点给出明确判断。没有人会手工审查一份5000页的证明，更不用说那份在 Harmonic 2023年成立时激发其想象的、假设有100000页的黎曼猜想证明。Labenz 指出，DeepMind 在2024年从形式化的 AlphaProof 转向了今年的非正式 Gemini，而 OpenAI 的 IMO 系统也是非正式的；训练可能继续采用混合方式，但 Harmonic 认为形式化与非形式化输出之争已经“尘埃落定”。
9. AI 编写软件带来与 AI 数学相同的验证瓶颈
创始人把长证明的逻辑直接延伸到了代码。Cursor 团队的一项实验生成了一个约150万行、兼容 Chromium 的浏览器；当智能体自主工作数周后，无论人类还是协作模型，都不可能以经济可行的方式检查每一行代码是否存在漏洞。如果这类系统要成为可靠的基础设施，验证成本的增长速度就必须远低于生成复杂度。
Tenev 质疑，AI 生成的代码是否还应继续使用 Python 或 Java——这些语言的设计部分考虑了人类可读性。如果机器是主要作者，形式上可验证的语言或许是更好的目标，因为系统可以直接建立性质，而不是从测试和代码审查中推断性质。Lean 是 Harmonic 最喜欢的语言，但创始人也承认，采用情况仍然是开放问题。
扩散应当从任务关键型系统开始，因为这些系统的缺陷代价格外高，团队也已经在聘用 Lean、Rocq 或 Isabelle 专家，进行耗时的验证。Aristotle 可以先加速这些专家，再把实践扩展到“形式化氛围编程”。设想中的终点不只是更快的编程，而是越来越少漏洞的软件，其安全性和可靠性声明都带有机器可检查的证书。
10. 新抽象需要熵，而不是逃离逻辑
Labenz 最尖锐的形而上学反驳是：在今天的形式系统中训练，是否会把 AI 困在今天的抽象里？Einstein 推翻了直觉上的三维世界观，因此数学超级智能或许也必须“打破第四面墙”。Achim 的回答是，Einstein 仍然可以通过微分几何严谨表达这一突破；任何通过独立可检查的推导推进的新理论，本身都可以编码进 Lean。
Lean 的公理旨在描述极其基本的推理操作，而不是某一种特定的物理范式。因此 Achim 把形式化推理视为非正式推理的一个极其细致、可由计算机检查的版本，而不是概念牢笼。哥德尔式不完备性会把真实但不可证明、不可判定的命题留在前沿，但创始人并不认为这些边界情况会妨碍证明“绝大多数有用的东西”。
在这一框架内，熵仍然不可或缺。Aristotle 会尝试许多最终失败的路径，而这些失败让它能够触及人类从未写下的思想；“幻觉是推理系统的关键组成部分”。理想设计不是一个零幻觉生成器，而是一个与形式验证器耦合的高熵探索者：它能够提出错误命题，发现命题错误，然后只保留经过认证的结论。
11. 终局是受实验约束的理论丰饶
Harmonic 的既定路径始于2023年成立，经过2025年 IMO 金牌水平表现、年终基准测试登顶，以及 API 用户解决那些曾经开放了30年或40年的中等难度问题。下一个飞轮很直接：自动形式化扩充 Mathlib，更大的认证库降低困难证明的成本，用户继续追逐更重要的猜想，而几乎每天的产品改进则降低提交工作的摩擦和成本。
Achim 对2030年的渐近状态描述为“基本上能够解释一切的理论”。科学界不再需要艰难寻找量子力学与广义相对论之间任何一个自洽的桥梁，而可能拥有5种能够解释全部现有观测的竞争性统一理论。届时瓶颈将重新回到数据：研究人员需要越来越高能的实验，甚至可能需要新的对撞机，才能判断哪一种数学上自洽的解释描述了真实宇宙。
这个判断明确不等于全知。模型只能从有现实依据的假设和观测出发进行推理；宇宙的某些性质“只能运行实验，亲自找出答案”。但 Achim 预计，在达到那个渐近状态之前，系统就会产生巨大的效用：消除能够持续进行高水平逻辑推理的人才短缺，可能带来一场科学复兴。
今天的安全性部分来自受限的行动空间：Aristotle 输出 Lean 文件，而不是自主接触 Gmail、iMessage 或运营系统。Tenev 预计，一旦智能体与更多系统连接，最初的严重风险将类似于由 API 和自主执行引发的网络安全事件。随着 Harmonic 最终把模型接入现实世界，Achim 表示，公司必须更加认真地对待这些风险，同时保留其治理原则：“人类应该掌舵并作出决定。”