股票交易平台 Robinhood 的 CEO Vlad Tenev 此前创办的 AI 公司再次获得资本市场青睐。7 月 9 日，他与合伙人共同创办的 AI 初创公司 Harmonic 宣布完成 1 亿美元 B 轮融资，公司估值达到 8.75 亿美元，接近独角兽门槛。这轮融资由知名风投机构 Kleiner Perkins 领投，Paradigm 等多家机构跟投。
这家成立仅两年的公司专注于一个颇为前沿且具有挑战性的领域——数学超级智能（MSI，Mathematical Superintelligence）。与目前主流的大语言模型（LLM，Large Language Model）不同，Harmonic 试图从根本上解决 AI“幻觉”问题，即模型编造虚假信息的现象。他们的解决方案是让 AI 掌握严谨的数学推理能力，通过形式化验证确保每一个推理步骤都是可验证的。
能够在这个极其专业的领域取得突破，很大程度上源于 Vlad Tenev 深厚的数学功底。这位保加利亚裔美国企业家 5 岁时随父母移居美国，在弗吉尼亚州的托马斯·杰斐逊科学技术高中就读，随后进入美国斯坦福大学攻读数学学士学位。在斯坦福期间，他遇到了后来的 Robinhood 联合创始人 Baiju Bhatt。大学毕业后，Tenev 进入美国加州大学洛杉矶分校（UCLA）攻读数学博士学位，师从著名数学家的陶哲轩。
在 UCLA 的求学经历对 Tenev 影响颇大。陶哲轩以其在多个数学领域的卓越贡献而闻名，从数论、组合学到调和分析，他都有开创性工作。更重要的是，陶哲轩近年来积极参与 Lean 编程语言的推广——而这种语言正是 Harmonic 技术路线的核心。
不过，尽管拥有深厚的数学功底，Tenev 最终却选择从 UCLA 博士项目退学，与 Bhatt 一起在纽约创办了两家金融科技公司，分别是高频交易软件公司 Celeris 和为交易公司提供低延迟软件的 Chronos Research。这些早期经历为他们后来创办 Robinhood 积累了宝贵经验。2013 年，瞄准传统券商高昂手续费带来的市场准入门槛，他们创办了 Robinhood，以零佣金交易模式颠覆了行业格局。
Harmonic 的另一位联合创始人 Tudor Achim 同样来头不小。他拥有美国卡内基梅隆大学计算机科学学士学位，曾在斯坦福大学攻读计算机科学博士，专注于 AI 在感知领域的应用。更重要的是，Achim 是自动驾驶公司 Helm.ai 的联合创始人兼前 CTO，该公司为全球多家顶级汽车制造商提供 AI 解决方案。他在机器学习和算法领域的深厚背景，与 Tenev 的数学专长形成了互补。
两人的合作始于对一个共同愿景的追求——利用 AI 解决千禧年大奖难题中的某个数学问题。当 Tenev 和 Achim 开始认真思考这个可能性时，他们意识到，传统的 AI 方法根本无法胜任如此复杂的数学推理任务。
而他们最终找到的答案是 Lean 编程语言。这种由微软研究院的 Leonardo de Moura 开发的函数式编程语言，最初是为软件验证而设计的，但意外地在数学界获得了巨大成功。Lean 的独特之处在于，它可以将数学定理表述为可验证的代码，任何在 Lean 中编译通过的证明都保证是逻辑正确的。
基于这一技术路线，Harmonic 开发出了核心产品 Aristotle 模型。当用户用自然语言提出数学问题时，Aristotle 能够将问题形式化为 Lean 4 代码，通过严格的逻辑推理求解问题，并将答案同时用自然语言和 Lean 代码输出。这种“自动形式化”能力让 Aristotle 能够与不熟悉 Lean 语言的数学家和教育工作者协作，检查他们的工作并填补细节。
得益于这些特殊设计，Aristotle 在数学上的表现十分突出。在数学推理领域的标准基准测试 MiniF2F 上，Aristotle 达到了 90% 的正确率，创下了新的业界纪录，远超此前 DeepSeek-Prover 的约 60% 和 LEGO-prover 的约 50%。要知道，MiniF2F 包含 488 个来自国际数学奥林匹克竞赛和高中、本科数学课程的问题，难度跨度从简单计算到极具挑战性的证明，其中验证集甚至包含三个来自国际数学奥林匹克的问题。
更重要的是，Harmonic 在技术路线上实现了几个关键突破。首先是递归自我改进能力。由于 Lean 提供了客观的验证标准，Aristotle 可以通过强化学习和自我对弈快速迭代改进，这在其他 AI 领域很难实现，因为缺乏明确的奖励函数。其次是合成数据生成优势。与许多 AI 公司面临的数据稀缺问题不同，Harmonic 可以生成大量合成数学数据来训练模型，通过从简单概念逐步构建更复杂问题，模拟人类学习数学的过程。
这种技术路线与当前主流的大语言模型存在本质差异。现有的 LLMs 通过学习互联网上的文本数据来获得能力，但在数学推理方面往往力不从心，容易产生幻觉。Harmonic 认为，数学是推理的语言，掌握了数学推理能力的 AI 系统在科学、工程等需要严谨逻辑的领域都会表现出色。如 Achim 所说：“当人们在数学方面变得非常优秀时，他们往往在科学和工程的其他定量领域也表现出色。”
从商业前景来看，Harmonic 瞄准的是高风险、对准确性要求极高的应用场景。在航空航天、芯片设计、工业系统和医疗健康等领域，软件可靠性至关重要，传统 AI 的不确定性使其难以胜任。Harmonic 的形式化验证能力可以确保关键软件的正确性，这在区块链、金融服务等对安全性要求极高的行业具有巨大价值。Tenev 预测，随着 AI 能力的提升，未来 5 到 10 年内，绝大多数软件都将是经过验证的、可证明正确的。
当然，目前数学界对 AI 数学的态度并不都是如此乐观。虽然年轻数学家普遍对 AI 和 Lean 等验证工具持积极态度，但年长的学者则相对谨慎。Tenev 认为这种态度将会逐渐变化，一如国际象棋领域的发展轨迹——最初是人机协作，随着 AI 能力提升，最终 AI 将在纯粹的问题求解方面超越人类，而人类数学家的角色将转向指导 AI、解释结果和决定研究方向。
Harmonic 团队显然对未来充满信心。Tenev 援引预测平台 Metaculus 的数据，称下一个千禧年大奖难题有 43% 的可能性由 AI 或人机协作解决，但他认为这个比例被严重低估了。他的预测更加激进：如果下一个难题还由人类独立解决，那必须发生在很近的将来，而再下一个几乎肯定会有 AI 的重要贡献。他甚至预测 2026 年可能攻克相对简单的 Navier-Stokes 方程问题，2029 年解决黎曼猜想。
这样的雄心也获得了投资方的强烈认同。Kleiner Perkins 的合伙人 Ilya Fushman 此前本身就是一位物理学家，他表示：“Harmonic 创造了一个可验证、可扩展推理的新基础，可以在高风险环境中得到信任。我对 Aristotle 的应用前景深感兴奋，不仅仅是在软件领域，更是在加速科学、工程和通用智能发展上。”Index Ventures 的合伙人 Jan Hammer 将加入董事会担任观察员，他认为数学超级智能将产生巨大影响，就像 Google 让我们能够瞬间回答简单问题一样，Harmonic 可能让我们轻松运行复杂的数值求解器、优化工业设置、验证代码等。
值得一提的是，Harmonic 的出现也恰逢其时。一方面，自回归语言模型在过去几年取得了显著进步，使得在无限动作空间中的预测成为可能——这正是数学推理所需要的能力，因为在数学中你可以生成任何下一步推理。另一方面，Lean 4 在 2023 年 9 月才正式发布，为大规模数学形式化提供了成熟的基础设施。这两个关键技术的成熟，为 Harmonic 的技术路线提供了坚实基础。
随着 B 轮融资的完成，Harmonic 计划将资金主要用于加速 Aristotle 模型的开发和商业化应用。公司目前正在积极招聘 AI 研究员、数学家和分布式系统专家，希望在数学超级智能这一前沿领域保持领先优势。按照计划，Aristotle 模型将在今年晚些时候向研究人员和普通公众开放，这将是验证其技术路线可行性的重要里程碑。
参考资料：
1.https://www.bloomberg.com/news/articles/2025-07-10/robinhood-ceo-s-ai-math-startup-valued-at-nearly-900-million?embedded-checkout=true
2.https://www.sequoiacap.com/podcast/training-data-harmonic/
3.https://harmonic.fun/news
排版：刘雅坤
