務工家庭走出00后天才！退學造110億獨角獸，終身教授辭職追隨

2億美元A輪融資，估值110億，成立僅一年就成為獨角獸。更震撼的是創始人——25歲的廣州00后洪樂潼，父母是從未上過大學的普通務工者。她用數學解決AI最大的痛點：讓模型推理步步可驗證，徹底杜絕幻覺。為了加入她，弗吉尼亞大學終身教授直接辭職。

就在上周，全球創投圈被一個名字刷屏了。

AI初創公司Axiom宣布完成2億美元A輪融資，由硅谷頂級風投Menlo Ventures領投，Greycroft、Madrona Venture、B Capital、Toyota Ventures等老股東全部跟投。公司估值飆升至16億美元。

成立不到一年，直接躋身獨角獸。

但更讓人震撼的，是這家公司的創始人——25歲的洪樂潼（Carina Hong）。

她讓大模型的推理過程像數學證明一樣嚴格，每一步都可驗證。

17歲進MIT，3年修完雙學位

洪樂潼祖籍潮汕，出生在廣州，父母是普通務工者，但她從小就展現出極其罕見的數學天賦。

高一時，她入選廣東省中學生英才計劃，師從中山大學教授王學欽。

隨后，她在全國中學生數學奧林匹克（CMO）廣東選拔中脫穎而出，成為僅有的四位女生之一。

2018年，17歲的洪樂潼被麻省理工學院（MIT）錄取，選擇了數學與物理雙專業。

接下來的履歷，堪稱「開掛」。

她在MIT只用3年就修完兩個學位，本科期間發表了9篇學術論文，研究方向涵蓋模橢圓曲線、K3曲面上的L函數、「月光猜想」等基礎數學領域。

她曾獲得全美女性數學家最高榮譽——Alice T. Schafer數學獎，以及表彰北美數學專業本科生杰出研究的AMS-MAA-SIAM摩根獎 。

2021年，洪樂潼獲得牛津大學羅德獎學金，成為當年僅有的四位中國獲獎者之一。

羅德獎學金被譽為「本科諾貝爾獎」，是世界上歷史最悠久、最負盛名的國際獎學金項目。

在牛津攻讀神經科學碩士期間，她在倫敦大學學院蓋茨比計算單位作為第一作者開展深度學習研究，正式踏入AI領域。

隨后她又進入斯坦福大學，攻讀數學與法律雙學科博士。

但博士還沒讀完，她就退學了。

AI的致命缺陷：概率模型沒有「絕對正確」

洪樂潼看到的，是AI行業最尖銳的矛盾。

大模型的能力在狂飆，但可靠性始終是個黑盒。

日常應用中的胡說八道或許無傷大雅，但在金融、國防、關鍵基礎設施領域，任何基于概率的錯誤都可能釀成災難。

去年針對ChatGPT o3「數學測試作弊」爭議，作為斯坦福數學博士的洪樂潼率先指出癥結：當前AI缺乏嚴格的邏輯推理訓練體系。

現有的大模型本質上是概率機器。它們通過海量數據學習模式，然后基于統計規律給出答案。

即使是GPT-4、Claude這樣的頂級模型，其概率性的本質依然是主要的擔憂原因。

洪樂潼的答案是：讓AI像數學家一樣工作。

她創立的Axiom采用「數學即服務」模式，通過訓練AI系統生成用Lean語言編寫的、經過形式化驗證的輸出。

Lean是一種專為數學證明設計的編程語言，通過使用Lean，Axiom可以確保AI模型推理過程的每一步都是可機器檢查的并且在邏輯上得到保證。

傳統大模型給你一個答案，你只能信或不信。而Axiom的系統給你一個答案，同時附帶一個完整的、可驗證的證明過程，不存在大概是對的這種模糊地帶。

洪樂潼在接受采訪時說：

科學突破往往需要兩步：提出假設，再用證明去驗證。我們創立Axiom，就是要無限壓縮把好奇心轉化為真理的時間。

滿分通過普特南競賽，攻克20年數論猜想

去年12月，Axiom交出了第一張成績單。

Axiom的核心系統在普特南競賽中，斬獲滿分，12題全對。

普特南競賽是北美地區最負盛名的大學生數學競賽，成績的中位數常常為零（滿分120分）。

過去近百年，僅有5人達成過滿分成就。Axiom的AI做到了。

更震撼的還在后面。Axiom可驗證地證明了一個已有20年歷史的數論猜想，該猜想涉及用于測量曲面距離的微積分元素。

這個問題，連Axiom的創始數學家Ken Ono都曾多年嘗試未能解決。

去年12月，Axiom開發的AxiomProver系統，使用可驗證的Lean語言，完成了埃爾德什問題集中第124題和第481題的形式化證明，分別用時1天和5小時，全程無人為干預。

埃爾德什問題集共包含1109個關于組合數學和數論的問題，是匈牙利數學家保羅·埃爾德什數十年來論文的匯集。

迄今為止，只有266個問題被證明，其中僅10個問題的證明被轉化為計算機可驗證的形式化版本。

解決數學問題只是冰山一角。Axiom正在將這種「絕對正確」的數學推理能力，通過遷移學習引入到代碼驗證領域，試圖解決生成式AI的種種問題。

目標客戶是對沖基金、量化交易員等高端場景。這些地方，容不得半點「大概對」。

終身教授辭職加入，只因「見證了數學超級智能的可能」

Axiom最震撼的一次招聘，發生在去年12月。

Ken Ono（小野健），弗吉尼亞大學Marvin Rosenblum講席教授、前美國數學學會副主席，辭去終身教職，全職加入Axiom擔任創始數學家。

他是古根海姆獎、帕卡德獎、斯隆獎得主，世界頂尖的拉馬努金數學權威之一 ，還是電影《知無涯者》的副制片人和數學顧問，甚至出演過百威啤酒的超級碗廣告。

并且，他也是唯一一位出演過啤酒廣告的數論學家。

在Ken Ono長達四十年的執教生涯中，曾指導過十位摩根獎得主，洪樂潼正是其中之一。

為什么一個功成名就的終身教授，會放棄穩定的學術生涯，去為一個25歲的年輕人工作？

華爾街日報報道稱，Ken Ono在人工智能徹底改變他的職業生涯和生活之前，一直對人工智能持懷疑態度。

直到最近，他開始談論人工智能時，還總是嘲諷圍繞這項新興技術的炒作 。

但見到Axiom的系統后，他頓悟了。

除了Ken Ono，Axiom的團隊堪稱「夢之隊」：

CTO Shubho Sengupta曾任Meta AI研究總監，此前參與過Google分布式訓練系統的研究工作，也是最早開發CUDA技術的專家之一 ；

核心科學家Fran?ois Charton，是率先將Transformer模型引入數學領域的先驅，曾用大模型推翻過一個長達30年未解的學術猜想。

一位投資人忍不住感慨：

她兼具深厚的數學功底、驚人的運營效率，以及吸引世界一流人才的能力。這是我過去二十年的硅谷生涯中，見過的最令人印象深刻的創始人，沒有之一。

目前，Axiom擁有30多名員工，招聘速度還在不斷加快。

00后集體登場，AI創業進入「理想主義者」時代

就在上周，成立僅一年多的公司靈初智能宣布完成天使輪及Pre-A輪共計20億元融資。

其聯合創始人陳源培，出生于2001年，曾就讀于北京大學、斯坦福大學，師從李飛飛。

同為00后的楊豐瑜在耶魯博士畢業后選擇回國創業，2024年成立了具身智能公司優理奇，完成數億元的天使輪及天使+輪融資。

2025年，由三位00后創立的AI招聘網站Mercor也宣布完成1億美元的B輪融資，公司估值達20億美元。

這一代創業者，和上一代有什么不同？

曾在DeepSeek火爆全球之際，洪樂潼發出這樣的感慨：

一個小而專注、特立獨行的團隊。一群理想主義者組成的優秀合作伙伴。他們執行力強，親力親為。最珍貴的，是那份理想與使命交織的信念。這就是DeepSeek的故事，也是我想親自書寫的故事。

有投資人私下交流時回憶，洪樂潼在創立Axiom期間于朋友圈寫下的自勉：

祝自己做花也做樹。繽紛熱情，孤離兀立。

談話間，她幾乎不談論風口與顛覆，更多在意對問題本身的好奇和對技術可能性的清晰判斷。

對于Axiom的終極使命，洪樂潼留下了一句極具張力的注腳：

Verified AI關注的，絕不僅僅是修補AI的缺點。真正瞄準的，是AI的上限，是通向超級智能的階梯。

從廣州普通家庭走出的女孩，到掌舵估值110億的AI獨角獸。

從MIT的數學天才，到讓終身教授辭職追隨的創業者。

洪樂潼和她這一代00后創業者的故事，正在改寫硅谷的敘事規則：不是為了風口而創業，而是為了解決真正困難的技術問題。

AI的上限在哪里？或許答案就藏在這群25歲年輕人的選擇里。

參考資料：

https://mp.weixin.qq.com/s/msJXxZMSyfXMXDPMCdtznQ