来源：DeepTech深科技
股票交易平台Robinhood 的 CEO Vlad Tenev此前创办的 AI 公司再次获得资本市场青睐。7 月9 日，他与合伙人共同创办的AI 初创公司 Harmonic 宣布完成1 亿美元B 轮融资，公司估值达到8.75 亿美元，接近独角兽门槛。这轮融资由知名风投机构Kleiner Perkins 领投，Paradigm 等多家机构跟投。
Harmonic（来源：Harmonic）
这家成立仅两年的公司专注于一个颇为前沿且具有挑战性的领域——数学超级智能（MSI，Mathematical Superintelligence）。与目前主流的大语言模型（LLM，LargeLanguageModel）不同，Harmonic 试图从根本上解决AI“幻觉”问题，即模型编造虚假信息的现象。他们的解决方案是让AI 掌握严谨的数学推理能力，通过形式化验证确保每一个推理步骤都是可验证的。
能够在这个极其专业的领域取得突破，很大程度上源于Vlad Tenev 深厚的数学功底。这位保加利亚裔美国企业家5 岁时随父母移居美国，在弗吉尼亚州的托马斯·杰斐逊科学技术高中就读，随后进入美国斯坦福大学攻读数学学士学位。在斯坦福期间，他遇到了后来的Robinhood 联合创始人Baiju Bhatt。大学毕业后，Tenev 进入美国加州大学洛杉矶分校（UCLA）攻读数学博士学位，师从著名数学家的陶哲轩。
Vlad Tenev（来源：UCLA Mathematics）
在UCLA 的求学经历对Tenev 影响颇大。陶哲轩以其在多个数学领域的卓越贡献而闻名，从数论、组合学到调和分析，他都有开创性工作。更重要的是，陶哲轩近年来积极参与Lean 编程语言的推广——而这种语言正是Harmonic 技术路线的核心。
不过，尽管拥有深厚的数学功底，Tenev 最终却选择从UCLA 博士项目退学，与Bhatt 一起在纽约创办了两家金融科技公司，分别是高频交易软件公司Celeris 和为交易公司提供低延迟软件的Chronos Research。这些早期经历为他们后来创办Robinhood 积累了宝贵经验。2013 年，瞄准传统券商高昂手续费带来的市场准入门槛，他们创办了Robinhood，以零佣金交易模式颠覆了行业格局。
Harmonic 的另一位联合创始人Tudor Achim 同样来头不小。他拥有美国卡内基梅隆大学计算机科学学士学位，曾在斯坦福大学攻读计算机科学博士，专注于 AI 在感知领域的应用。更重要的是，Achim 是自动驾驶公司Helm.ai 的联合创始人兼前CTO，该公司为全球多家顶级汽车制造商提供AI 解决方案。他在机器学习和算法领域的深厚背景，与Tenev 的数学专长形成了互补。
Tudor Achim（来源：SequoiaCapital）
两人的合作始于对一个共同愿景的追求——利用AI 解决千禧年大奖难题中的某个数学问题。当Tenev 和Achim 开始认真思考这个可能性时，他们意识到，传统的AI 方法根本无法胜任如此复杂的数学推理任务。
而他们最终找到的答案是Lean 编程语言。这种由微软研究院的Leonardo de Moura 开发的函数式编程语言，最初是为软件验证而设计的，但意外地在数学界获得了巨大成功。Lean 的独特之处在于，它可以将数学定理表述为可验证的代码，任何在Lean 中编译通过的证明都保证是逻辑正确的。
基于这一技术路线，Harmonic 开发出了核心产品Aristotle 模型。当用户用自然语言提出数学问题时，Aristotle 能够将问题形式化为Lean 4 代码，通过严格的逻辑推理求解问题，并将答案同时用自然语言和Lean 代码输出。这种“自动形式化”能力让Aristotle 能够与不熟悉Lean 语言的数学家和教育工作者协作，检查他们的工作并填补细节。
提供给Aristotle 用于自动形式化 2001 年国际数学奥林匹克竞赛第 6 题解答的原始提示（来源：Harmonic）
得益于这些特殊设计，Aristotle 在数学上的表现十分突出。在数学推理领域的标准基准测试MiniF2F 上，Aristotle 达到了 90% 的正确率，创下了新的业界纪录，远超此前DeepSeek-Prover 的约60% 和LEGO-prover 的约50%。要知道，MiniF2F 包含488 个来自国际数学奥林匹克竞赛和高中、本科数学课程的问题，难度跨度从简单计算到极具挑战性的证明，其中验证集甚至包含三个来自国际数学奥林匹克的问题。
MiniF2F 基准上的评测结果（来源：Harmonic）
更重要的是，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
排版：刘雅坤