25歲的洪樂潼，最近在硅谷火了。

這個來自廣東的女孩，17歲考入MIT，三年修完數(shù)學(xué)和物理雙學(xué)位，后來又進(jìn)入斯坦福深造。

按照硅谷最熟悉的那套敘事，她是“天才少女創(chuàng)業(yè)者”的模板人物。

但洪樂潼真正讓人記住的，不是履歷，而是她做的事太反常識。

當(dāng)整個AI行業(yè)都在追逐更大的模型、更強(qiáng)的生成能力、更像人的表達(dá)時，她偏偏轉(zhuǎn)身去做了一件最不性感、也最難商業(yè)化的事：用數(shù)學(xué)驗(yàn)證AI。

她創(chuàng)辦的公司叫Axiom，成立不足兩年，員工只有20多人，最近拿下2億美元A輪融資，投后估值高達(dá)16億美元，折合人民幣超110億元。

Axiom不做聊天機(jī)器人，不做文生圖，也不跟風(fēng)大語言模型的熱潮。它做的是“形式化驗(yàn)證”。

說白了，就是想用數(shù)學(xué)和邏輯，把AI每一步推理都變成可以檢查、可以證明、可以追責(zé)的東西。

這聽起來很冷門，但它瞄準(zhǔn)的，卻是大模型最麻煩的軟肋——幻覺。

現(xiàn)在的AI最大的問題不是不夠強(qiáng)，而是不夠可靠。它可以把答案說得很像對的，甚至真的做對題，但你沒法確認(rèn)它到底是真的推出來了，還是只是“猜對了”。而Axiom要做的，就是把這種模糊狀態(tài)，變成一種可驗(yàn)證的確定性過程。

這也是為什么，當(dāng)洪樂潼拿著這個想法去融資時，迎面撞上的不是掌聲，而是一個極其現(xiàn)實(shí)的問題：“數(shù)學(xué)怎么賺錢？”

01

迎難而上的天才少女

洪樂潼的辦公室在硅谷帕洛阿爾托大學(xué)大道，距離斯坦福大學(xué)步行只要半個小時。斯坦福是她博士生涯的起點(diǎn)，但學(xué)位還沒有念完，她就退學(xué)創(chuàng)業(yè)了。

事實(shí)上，早在博士在讀期間，洪樂潼就已經(jīng)注冊了公司。公司取名Axiom，名字源自數(shù)學(xué)術(shù)語“公里”，“我想從公理出發(fā)，打造一個能夠自我改進(jìn)的超級智能推理器?！?/p>

一個24歲的博士生，沒錢沒人沒產(chǎn)品，僅憑一個想法，她就拿下了960萬美元的種子輪投資。

憑什么？

要知道現(xiàn)有的大模型本質(zhì)上是概率黑盒，通過海量數(shù)據(jù)學(xué)習(xí)模式，然后基于統(tǒng)計(jì)規(guī)律給出答案。推理過程無法被量化，所以會胡說、會出錯。

洪樂潼要做的就是用數(shù)學(xué)公理和形式化驗(yàn)證，讓AI每一步推理都可證明，可以直接面向金融、軍工、芯片和自動駕駛等對可靠性要求極高的市場。

她做的事顯然擊中了AI 最大痛點(diǎn)，解決幻覺與可靠性的問題。

更何況，早期投資投人，她本人也是不折不扣的跨學(xué)科天才學(xué)霸。

洪樂潼從小就展現(xiàn)出了驚人的數(shù)學(xué)天賦。2001年，她出生于廣州市天河區(qū)，曾就讀于華南師大附中。高一時，她就在全國數(shù)學(xué)奧林匹克選拔賽中晉級，并在華羅庚杯、全國高中數(shù)學(xué)聯(lián)賽中屢獲佳績。

正是在奧數(shù)集訓(xùn)中，她對研究型數(shù)學(xué)產(chǎn)生了興趣。

2018年，17歲的她被MIT錄取，3年就修完了數(shù)學(xué)和物理雙學(xué)位，不僅發(fā)表了9篇學(xué)術(shù)論文，還獲得全美女性數(shù)學(xué)家最高榮譽(yù)Alice T. Schafer數(shù)學(xué)獎等諸多榮譽(yù)。

此后，她獲得牛津大學(xué)羅德獎學(xué)金，她沒有繼續(xù)深耕數(shù)學(xué)，轉(zhuǎn)頭去學(xué)了神經(jīng)科學(xué)，因?yàn)橄搿皹?gòu)建跨越科學(xué)領(lǐng)域的認(rèn)知體系”。

基于這一目標(biāo)，她同時在倫敦大學(xué)學(xué)院蓋茨比計(jì)算神經(jīng)科學(xué)中心開展深度學(xué)習(xí)研究，該中心由“深度學(xué)習(xí)之父”杰弗里·辛頓聯(lián)合創(chuàng)立。也正是在此期間，她正式踏足AI領(lǐng)域，接觸到許多最前沿的課題。隨后她又進(jìn)入斯坦福大學(xué)，攻讀數(shù)學(xué)與法律雙學(xué)科博士。

2024年，ChatGPT o3被曝光在數(shù)學(xué)測試中存在“作弊”嫌疑，全球輿論嘩然。

作為斯坦福數(shù)學(xué)博士的洪樂潼也在社交媒體上發(fā)表了看法：“OpenAI大模型在數(shù)學(xué)測試中表現(xiàn)優(yōu)秀，大概率是因?yàn)橛?xùn)練數(shù)據(jù)中提前泄題了。在一些測試中，大模型回答的準(zhǔn)確率雖然高達(dá)96%，但一旦展示推理過程，得分率就降至5%?！?/p>

面對行業(yè)痛點(diǎn)，一種名為Lean的語言闖入她的視線，也讓她嗅到了創(chuàng)業(yè)機(jī)會。

與自然語言不同，Lean語言是一個非常神奇的、可以自驗(yàn)證的數(shù)學(xué)編程語言。洪樂潼打了個比方：“如果用英語寫出數(shù)學(xué)證明，我沒辦法知道一個5000行的證明是否正確，需要找高水平的專家驗(yàn)證。但Lean是自驗(yàn)證的，只要跑通了就是對的?！?/p>

Lean的邏輯是把自然語言或非形式化驗(yàn)證，轉(zhuǎn)成機(jī)器可檢查的形式化驗(yàn)證。

那啥是形式化驗(yàn)證呢？

普通的AI，你只能用它的答案來判斷它是不是理解這個問題，但你不知道它中間有沒有瞎蒙。

形式化驗(yàn)證是要求你把每一步都寫成機(jī)器能檢查的邏輯鏈條。只要中間有一步跳了、糊了、偷懶了，它就不給過。

之所以形式化驗(yàn)證能治大模型會幻覺，是因?yàn)樾问交?yàn)證不管你答案如何，只要你的結(jié)論是從前提里一步步合法推出來的，那答案就是對的，從而避免了模型產(chǎn)生幻覺。

所以Axiom做的，就是讓大模型負(fù)責(zé)猜想和搜索，讓Lean負(fù)責(zé)驗(yàn)算和判斷。如果Lean檢查發(fā)現(xiàn)過程不對，那就退回去繼續(xù)改。

但這顯然是一條窄路。這條路冷門到什么程度？在整個AI版圖里，形式化驗(yàn)證幾乎是邊緣中的邊緣，全球的商業(yè)化玩家一只手就數(shù)得過來。

顯然她并不是因?yàn)樾问交?yàn)證是下一個風(fēng)口才選的，而是因?yàn)樗龑Α袄щy”的定義和別人不一樣。

奧賽就像持續(xù)釋放多巴胺的快感，而研究型數(shù)學(xué)像在撞墻，充滿痛苦與煎熬。我其實(shí)特別喜歡這種挑戰(zhàn)感?！彼@樣解釋自己癡迷數(shù)學(xué)的原因。

正是這種刻在骨子里的挑戰(zhàn)欲，讓她不愿再停留在學(xué)術(shù)研究的舒適區(qū)，渴望在更廣闊的戰(zhàn)場上去攻克AI領(lǐng)域的硬骨頭。

2024年深秋，斯坦福附近的一家咖啡館里，洪樂潼與當(dāng)時Meta AI研究總監(jiān)Shubho Sengupta聊了整整幾個小時，核心議題只有一個：AI能不能真正學(xué)會數(shù)學(xué)推理？

兩人一拍即合，一個退學(xué)，一個辭職，兩人一起創(chuàng)業(yè)。

02

一支“草根”工程師軍團(tuán)

Axiom只有20多名員工，洪樂潼用了一個詞來形容團(tuán)隊(duì)的氣質(zhì)：草根工程師精神。

但事實(shí)上，這支團(tuán)隊(duì)的成員身份一點(diǎn)也不草根，甚至背景堪稱豪華。

Axiom第一位成員，正是和她在咖啡館聊了好幾個小時的Meta前員工Shubho Sengupta，如今他的身份是公司的CTO。

核心科學(xué)家Fran?ois Charton，則是將Transformer架構(gòu)引入數(shù)學(xué)推理領(lǐng)域的先驅(qū)人物。他干的活，就是把數(shù)學(xué)算式當(dāng)成一種“語言”輸入進(jìn)Transformer，試試看Transformer能不能像翻譯句子一樣去翻譯數(shù)學(xué)。

其他成員約半數(shù)來自Meta AI，另一半則是世界級數(shù)學(xué)家與形式化驗(yàn)證先驅(qū)。

而最讓外界震驚的一位成員，是57歲的數(shù)學(xué)泰斗小野?。↘en Ono）。

他是模形式領(lǐng)域的頂尖學(xué)者，美國數(shù)學(xué)學(xué)會前副會長，拿過古根海姆獎、斯隆獎等榮譽(yù)。指導(dǎo)過的學(xué)生中有十位摩根獎得主。他還曾為美國奧運(yùn)游泳隊(duì)提供數(shù)據(jù)分析，為電影《知無涯者》擔(dān)任顧問。

這位弗吉尼亞大學(xué)終身教授與洪樂潼結(jié)緣于麻省理工。彼時大一新生洪樂潼參與了他的數(shù)論項(xiàng)目。師生關(guān)系延續(xù)至今，角色卻已不同，2025年底，小野健辭去教職，全職加入Axiom，成為第15號員工。

曾拒絕過Google和Meta邀請的小野健，為什么愿意為一個24歲的學(xué)生“打工”？

“如果我的猜想能被機(jī)器在3天內(nèi)推廣到10個維度，我愿意當(dāng)一個‘標(biāo)注工’?！毙∫敖≡_表示，他選擇幫自己的學(xué)生打工，不僅因?yàn)楹闃蜂_出“不設(shè)教學(xué)、不設(shè)行政、100%科研”的合約，更關(guān)鍵的是，AI對他的“降維打擊”，讓他感到興奮。

一群頂級學(xué)者和前Meta成員，這個團(tuán)隊(duì)哪里草根了？

洪樂潼的解釋是，草根，代表著始終“空杯”的心態(tài)和堅(jiān)韌的品質(zhì)。在創(chuàng)業(yè)這條路上，即使是資深“牛人”，也要從頭學(xué)起，不斷自我革新。

她自己最喜歡的不是當(dāng)“精英”，而是做“草根”，做個nobody（小人物），這樣學(xué)習(xí)的坡度最陡、速度最快。

她自己也是“草根精神”的踐行者，在被問到如何帶領(lǐng)團(tuán)隊(duì)時，洪樂潼說：“我其實(shí)不太喜歡用帶領(lǐng)這個詞。我希望自己是一個Individual contributor（獨(dú)立貢獻(xiàn)者），每個人都是，這是一群志同道合的人在一起做事?！?/p>

“我們創(chuàng)立Axiom，就是要無限壓縮把好奇心轉(zhuǎn)化為真理的時間”，在資本驅(qū)動的硅谷，洪樂潼的這種純粹性，對于頂尖研究者而言，或許比一份高薪offer更有吸引力。

這支不到20人的團(tuán)隊(duì)，在成立后不到一年就交出了一份令人意外的答卷。

2025年12月3日，Axiom宣布其核心系統(tǒng)AxiomProver在無人干預(yù)的情況下，攻克了困擾數(shù)學(xué)界數(shù)十年的兩道埃爾德什難題。

同一天，洪樂潼收到了入選“福布斯30歲以下30人”榜單的消息。

同月，AxiomProver又在普特南數(shù)學(xué)競賽中斬獲滿分，12道題全對。普特南是北美最負(fù)盛名的大學(xué)生數(shù)學(xué)競賽，成績的中位數(shù)常常為零，過去近百年僅有5個人類選手拿到過滿分。

Axiom進(jìn)一步印證了用形式化驗(yàn)證構(gòu)建可靠、可核驗(yàn)、無幻覺的AI，已是行業(yè)明確的重要方向，而 AxiomProver 則在這條路徑上交出了可復(fù)現(xiàn)、高難度的實(shí)證。

03

賽道升溫，但挑戰(zhàn)剛剛開始

從行業(yè)發(fā)展來看，洪樂潼的選擇正好踩在了技術(shù)轉(zhuǎn)折點(diǎn)上。

2024年年底，Meta FAIR和斯坦福大學(xué)等多所機(jī)構(gòu)聯(lián)合發(fā)布了一篇立場論文《Formal Mathematical Reasoning: A New Frontier in AI》。

論文給出了這樣一個判斷，過去的AI數(shù)學(xué)就是喂很多數(shù)學(xué)題，再讓模型輸出答案。這就導(dǎo)致數(shù)據(jù)會污染、過程會胡編，AI沒辦法自判斷對錯，并且還很難復(fù)現(xiàn)過程。

這顯然是路走錯了。就拿乘法口訣表來說，里面寫的是2*3得6，那么你自己也能理解3*2就也得6。這個過程就叫復(fù)現(xiàn)。

論文主張的是下一步要把證明助手、形式系統(tǒng)、自動驗(yàn)證真正接進(jìn)模型里來，讓AI真正懂?dāng)?shù)學(xué)。

但這也意味著這條窄路正在變得擁擠。

過去十年，AI賽道的主流敘事是“更大參數(shù)、更多數(shù)據(jù)、更快生成”，所有大公司都在這條路上狂奔。洪樂潼選擇的形式化驗(yàn)證是其中冷門到幾乎沒有競爭的賽道。

今年年初，Meta也發(fā)布了半形式化推理技術(shù)，讓大語言模型能夠在不執(zhí)行代碼的情況下驗(yàn)證代碼補(bǔ)丁，準(zhǔn)確率高達(dá)93%。競品公司Harmonic在今年1月獲得了英偉達(dá)投資，估值達(dá)14.5億美元，產(chǎn)品已擴(kuò)展到代碼編寫和芯片設(shè)計(jì)領(lǐng)域。Theorem、Axiomatic AI、Cajal等一批初創(chuàng)公司，也在近兩年紛紛進(jìn)入這個賽道。

對Axiom而言，挑戰(zhàn)遠(yuǎn)不止行業(yè)競爭。

最大的挑戰(zhàn)在于商業(yè)模式。洪樂潼最初的設(shè)想是將產(chǎn)品服務(wù)于對沖基金和量化交易公司，快速解決與資產(chǎn)定價、股市預(yù)測相關(guān)的復(fù)雜數(shù)學(xué)問題。

但這個藍(lán)圖至今仍停留在構(gòu)想階段。對高頻交易而言，比“正確”更重要的是“足夠快”，毫秒級的延遲可能比一次罕見錯誤帶來更大損失。

Axiom的絕對正確性，在追求速度的金融場景中，其實(shí)際價值目前仍需要打一個問號。另一個挑戰(zhàn)，則在于除了對價格不敏感的航空航天、國防軍工等少數(shù)領(lǐng)域，其他絕大多數(shù)企業(yè)愿意為“絕對正確”支付高溢價嗎？

洪樂潼自己也承認(rèn)這一點(diǎn)：“數(shù)學(xué)怎么賺錢？我們從一開始就面臨這個挑戰(zhàn)?！钡J(rèn)為，“現(xiàn)在，商業(yè)信號已經(jīng)清晰很多，數(shù)學(xué)能創(chuàng)造價值，是因?yàn)樗茏晕因?yàn)證、自我檢查?！?/p>

另一方面，高估值本身也是一把雙刃劍。16億美元的A輪估值意味著，投資人期望的是超高速的增長和明確的退出路徑。

Axiom必須在未來一到兩年內(nèi)證明其技術(shù)具備規(guī)?；虡I(yè)化的可能，否則下一輪融資將面臨巨大壓力。與此同時，它需要在巨頭和強(qiáng)勁對手的夾擊中，用更少的資源跑出更快的速度。

Axiom的未來，更像是一場理想主義的壓力測試。 從“絕對正確”的技術(shù)理想，到“相對經(jīng)濟(jì)”的商業(yè)世界，Axiom的挑戰(zhàn)，才剛剛開始。