25歲的洪樂(lè)潼，最近在硅谷火了。

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

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

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

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

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

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

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

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

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

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

01

迎難而上的天才少女

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

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

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

憑什么？

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

普通的AI，你只能用它的答案來(lái)判斷它是不是理解這個(gè)問(wèn)題，但你不知道它中間有沒(méi)有瞎蒙。

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

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

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

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

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

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

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

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

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

02

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

03

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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