美国人工智能数学推理领域迎来新突破——专注于数学超级智能（MSI）开发的初创企业Harmonic宣布完成1.2亿美元C轮融资，公司估值跃升至14.5亿美元，正式跻身独角兽行列。值得注意的是，这家成立仅两年的企业尚未产生任何收入，却凭借技术实力获得资本市场的高度认可。
本轮融资由Ribbit Capital领投，红杉资本、Kleiner Perkins及爱默生基金会参与投资。资金将主要用于构建超大规模算力基础设施，以支撑其核心AI模型Aristotle的持续迭代。该模型通过将自然语言描述的数学问题转化为可验证的形式化语言，并使用编程语言Lean4输出推理过程，开创了"机器可验证"的数学解题新范式。据公司介绍，这种技术路径能有效消除传统AI模型常见的逻辑错误和事实偏差。
技术突破带来显著成果：今年7月，Aristotle在国际数学奥林匹克竞赛（IMO）中创造历史，成为首个对六道赛题中的五道给出形式化验证解答的AI模型。相关证明文档已公开上传至GitHub平台，供全球数学界审阅。公司联合创始人弗拉德·特涅夫透露，升级后的模型新增自然英语输入支持、自动引理生成功能，并优化了终端交互界面，开发者可通过API直接调用模型能力，移动端测试版应用也已同步上线。
支撑Aristotle的底层技术体系包含两大核心组件：内部研发的AI几何证明系统Yuclid，以及基于开源项目升级的自动化定理系统Newclid 3.0。前者专注于生成可验证的几何证明，后者则提供平面几何问题的求解能力。这种软硬协同的技术架构，使模型在处理复杂数学问题时展现出超越传统AI的可靠性。
资本市场的热情源于技术突破带来的想象空间。路透社分析指出，Harmonic在IMO竞赛中的表现，验证了自动化数学推理与形式化验证结合的技术路径可行性。公司另一位联合创始人图多尔·阿希姆强调，当前进展表明MSI技术正在加速数学及定量领域的发展，AI推理与形式化验证的深度融合将成为未来趋势。这位斯坦福计算机博士出身的技术领袖，此前曾创立自动驾驶企业Helm.ai并担任CTO。
值得注意的是，Harmonic的创始团队兼具学术深度与商业经验。特涅夫在创立Harmonic的同时，还担任金融科技公司Robinhood Markets的董事长兼CEO，而阿希姆则拥有丰富的AI系统开发经验。这种跨界组合为技术商业化提供了双重保障，或许正是资本愿意为尚未盈利的初创企业投入重金的关键因素。
