Mathematical Superintelligence

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 和自主性，网络安全风险会升高，并坚持“人类应该掌舵并作出决定”。

🔗 原始收听与视频来源： 数学超级智能：Harmonic 的 Vlad 与 Tudor 谈 IMO 金牌与万物理论