股票交易平臺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
排版：劉雅坤