★置頂zzllrr小樂公眾號《小樂數學科普》新鮮送到！

數學巨匠加盟00后青年洪樂潼的人工智能初創(chuàng)企業(yè)，架起人類直覺與機器邏輯的橋梁。

作者：圖靈APP（theturingapp.com）2026-4-10

譯者：zzllrr小樂（數學科普公眾號）2026-4-13

導讀

本文將探尋一個問題：為何一位享譽全球的數學天才，會放棄弗吉尼亞大學的終身教職，轉而效力于自己的門生 —— 洪樂潼（卡莉娜?洪，Carina Hong）創(chuàng)辦的公理數學（Axiom Math）公司。

數學界正在發(fā)生一項顛覆性變革：傳奇數論學家小野?。↘en Ono），正告別安穩(wěn)的學術生涯，投身于硅谷這場高風險的賽道角逐。我們將講述洪樂潼的崛起之路 —— 這位麻省理工學院的天才少女、羅德學者，從斯坦福大學退學創(chuàng)業(yè)，立志打造一臺不只是模仿解題思路，而是真正理解數學證明的智能機器。

小野健數十年來一直屹立于學術之巔，他曾擔任美國數學會副主席，還曾為好萊塢影業(yè)與奧林匹克賽事擔任顧問。他憑借數論與整數分拆領域的研究成果聲名遠揚，證明了一個世紀前斯里尼瓦瑟?拉馬努金發(fā)現的諸多神秘數學規(guī)律。

如今，57歲的他向終身教職所在的院校請了長假，加入公理數學公司 —— 這家初創(chuàng)企業(yè)的創(chuàng)始人，正是他24歲的門生洪樂潼。（上述年齡為去年的歲數，譯者注）

洪樂潼是一位天賦卓絕的實干家：她僅用三年就從麻省理工學院畢業(yè)，不僅斬獲摩根獎，還是一名羅德學者。由于覺得求學進度過于緩慢，她從斯坦福大學的法律與數學聯合學位項目退學。洪樂潼已籌集 6400 萬美元資金，從Meta等科技巨頭公司吸納頂尖人才，全力打造一臺 “機器數學家”。她的目標，是跳出數學競賽帶來的短暫快感，投身于數學研究那種充滿艱辛與磨礪的探索之中。

在競爭白熱化的賽道上，公理數學公司劍走偏鋒，選擇了一條融合之路。有些團隊專注于 Lean 等形式化語言，以求實現推導過程的絕對嚴謹；有些團隊則依托自然語言模型，主打直觀易懂的解題闡釋。而公理數學公司，正致力于尋找這兩者之間的黃金平衡點。他們將大語言模型的強大算力，與形式化驗證的邏輯一致性相結合，力求打造出一個既能自主驗證推導正確性，又能突破人類學術專業(yè)壁壘、發(fā)現全新真理的智能系統(tǒng)。

對小野健而言，此次跨界絕非為了名利。他拒絕了其他科技公司更為優(yōu)渥的邀約，只為投身一項足以載入史冊的事業(yè)。在親眼目睹人工智能模型在自己不擅長的領域超越自己后，他意識到，機器輔助的數學研究，正為人類探索宇宙提供一種全然不同的全新范式。如今，在帕洛阿爾托那間以高斯與圖靈之名命名的辦公室里，這位久經沙場的學術泰斗與朝氣蓬勃的天才少女并肩作戰(zhàn)，他們正用行動證明：當經驗的智慧與青春的活力相融共生，人類的知識版圖將迎來一場徹底的重塑。

一次出人意料的跨界：小野健加盟公理數學

“小野?。↘en Ono）是無數數學學子的偶像?！?洪樂潼在談及自己聘請這位昔日導師的決定時如此說道。小野健作為數學界的天才，數十年來一直屹立于學術之巔。他曾是弗吉尼亞大學數學系的終身教授，履歷輝煌得近乎不可思議。他正是那位將自學成才的天才數學家斯里尼瓦瑟?拉馬努金的研究成果，轉化為現代數學證明的學者。

2018至2021年間，小野健擔任美國數學會副會長。他還曾擔任奧運游泳選手的數學顧問，以及好萊塢導演的專業(yè)顧問。然而，即便對于像他這樣閱歷豐富、成就斐然的人來說，他做出的這個決定也堪稱出人意料。

57歲的他，毅然告別了在弗吉尼亞大學的安穩(wěn)生涯，放棄了鐵飯碗，投身于硅谷的一家初創(chuàng)企業(yè)。他選擇為一位24歲的年輕女性效力 —— 這位女性曾是他的學生，本身也是一位數學神童。

小野健素以數論領域的研究聞名于世。他專攻整數分拆這一奇妙領域，以及支配數字求和規(guī)律的隱藏結構。一個世紀前，拉馬努金首次發(fā)現了一些神秘的數學規(guī)律，小野健則證明了這些規(guī)律隸屬于一個更宏大的理論框架，并找到了讓這些規(guī)律變得可預測的法則。這項研究為他贏得了多項重要學術基金，也奠定了他數學界傳奇人物的地位。如今，他向學術界請了長假，且毫無歸期的打算。他跳槽到了由自己的門生 —— 洪樂潼創(chuàng)立的公司。

洪樂潼：從數學神童到初創(chuàng)公司CEO

洪樂潼絕非普通的 24 歲青年。她的天賦，足以讓許多功成名就的前輩都自愧不如。她僅用三年時間就從麻省理工學院完成了本科學業(yè)，斬獲了摩根獎 —— 這是美國本科數學研究者的最高榮譽。她還是一名羅德學者。

圖源：AMS美國數學會

在斯坦福大學攻讀法律與數學聯合學位期間，她覺得這條求學之路節(jié)奏太慢，于是選擇退學，創(chuàng)辦了公理數學（Axiom Math）公司。

洪樂潼已籌集到 6400 萬美元資金，立志打造出全球首款真正具備科研能力的機器數學家。她將目光投向了Meta等科技巨頭麾下的頂尖人才，四處招募該領域的先驅人物。而這之后，她找到了自己的導師。

洪樂潼的成長背景，根植于競爭激烈的數學競賽領域。她在中國長大，為了閱讀那些沒有中文譯本的高階教材，她自學了英語。年少時，她便在奧數集訓營中接受高強度訓練，在嚴格的時間限制下攻克一道道難題。

但最終，她發(fā)現這種靠競賽解題獲得的多巴胺快感，遠遠無法滿足自己的求知欲?！拔乙恢睂祵W領域的開創(chuàng)性發(fā)現抱有濃厚興趣。奧數競賽帶來的快感轉瞬即逝，但數學研究卻是一個反復碰壁、絞盡腦汁的過程，充滿了艱辛與磨礪。而我恰恰癡迷于這個部分。” 洪樂潼在接受《華爾街日報》采訪時如此解釋。

洪樂潼熱衷于鉆研法律與數學交叉領域的難題。在她看來，這兩個領域都是建立在嚴密邏輯之上的學科，需要同樣嚴謹的思維方式。但她看到了一個前所未有的機遇 —— 將二者以一種全新的方式融合起來。在斯坦福校園晨跑時，她常常琢磨著那句箴言：迎難而上，向最難的問題發(fā)起挑戰(zhàn)。她意識到，做數學研究固然艱難，但打造一臺能自主開展數學研究的機器，難度要大得多。而這，正是她無法抗拒的挑戰(zhàn)。

共同的目標：公理數學的創(chuàng)立初心

周末時，洪樂潼常常待在校園附近的一家咖啡館里。正是在那里，她邂逅了一位來自Meta公司的科學家Shubho Sengupta。兩人坐在一張公共桌旁交流，發(fā)現彼此都對同一個問題著迷：機器能否真正理解一個數學證明的內涵，而非僅僅預測證明過程中的下一個表述？他們探討如何將大語言模型的強大算力，與形式化驗證的邏輯一致性相結合。就在一次次這樣的交流中，公理數學公司應運而生。

“我們并非要打造另一個只會模仿解題思路的聊天機器人，而是要教會人工智能如何進行定理證明。這是一個本質上完全不同的挑戰(zhàn)，也是一項值得全力以赴的事業(yè)?！?洪樂潼在接受《越南快報》VnExpress采訪時表示。

公司的名字 “公理”（Axiom），源自數學中的基本概念 —— 作為理論體系出發(fā)點的不證自明的基本事實。洪樂潼希望打造的系統(tǒng)，不僅能解決數學難題，還能自主驗證自身推導過程的正確性；她希望這個系統(tǒng)具備真正的推理能力。其終極目標，是創(chuàng)造出一種超級智能，既能優(yōu)化物流系統(tǒng)，又能驗證關鍵軟件的安全性。

只要仔細審視當下的科技版圖，就不難發(fā)現這項技術蘊含的巨大商業(yè)潛力?！霸谖覀冄壑校瑪祵W即是代碼，代碼亦是數學。真正的魔力…… 源于人工智能、編程語言與數學三者的融合?！?洪樂潼在接受《思想經濟學》采訪時指出。

這項計劃的雄心壯志，與洪樂潼雷厲風行的行事風格相得益彰。她組建了一支特殊的團隊，成員既有年少成名的數學神童，也有經驗豐富的行業(yè)老兵。她坦言，團隊的目標絕非小打小鬧，而是要重塑人類的知識版圖。她深知，要實現這一目標，就必須架起一座橋梁，連通純粹數學的抽象世界與工程學的現實應用領域?！皵祵W是培養(yǎng)超級智能的絕佳試驗場?！?洪樂潼在接受《福布斯》雜志采訪時說道。

就在洪樂潼和小野健著手組建團隊之際，他們意識到自己正踏入一個競爭白熱化的賽道。打造一臺能像數學家一樣思考的機器，已成為人工智能垂直應用領域競爭最激烈的方向之一。各大科技巨頭，以及十幾家資金雄厚的初創(chuàng)公司，都在朝著這一目標全力沖刺。

2025年國際數學奧林匹克：機器登上領獎臺

2025年IMO國際數學奧林匹克競賽的落幕，標志著智能領域的格局迎來了一場變革。數十年來，這項賽事一直是選拔全球頂尖青少年數學人才的標桿。

但在這一年的競賽中，人工智能不僅參與了角逐，更一舉登上了領獎臺。OpenAI公司和谷歌深度思維（Deepmind）公司均宣布，其研發(fā)的實驗性推理系統(tǒng)在總分 42 分的競賽中斬獲 35 分，達到了金牌分數線。在六百余名人類參賽選手中，僅有約 10% 的人取得了同等佳績。

這兩套系統(tǒng)與人類選手遵循完全相同的嚴苛規(guī)則，在沒有互聯網接入、不借助任何外部工具的情況下，僅憑自身架構內嵌的邏輯算法，解出了六道題目中的五道。負責批改證明過程的往屆奧賽獎牌得主評價稱，機器給出的證明不僅完全正確，推導過程往往還異常清晰。盡管仍有五名少年選手取得了機器未能企及的滿分成績，但二者之間的差距正在迅速縮小。

“我并不想夸大其詞、制造恐慌，但在很多方面，這些大語言模型的表現，已經超越了全球絕大多數頂尖的研究生?！?小野健在一場關于自動化的公開討論中如此評價。

公理數學公司的競爭對手主要分為三大陣營。第一類是致力于研發(fā)基于 Lean、Isabelle 等定理證明語言系統(tǒng)的團隊。這類系統(tǒng)能夠讓計算機逐行驗證證明的每一個步驟，邏輯極為嚴謹，但往往缺乏人類數學家在探索新理論時所依賴的直覺思維。這種方法雖然過程緩慢、步步為營，卻能保證推導結果的絕對正確性 —— 這也是該陣營的首要目標。

第二類是自然語言處理團隊。這類團隊研發(fā)的模型，擅長用人類易于理解的語言闡釋數學問題。它們在提出新思路、尋找類比關系方面表現出色，但在構建形式化證明所需的絕對精確性上，卻常常力不從心。這些模型有時會展現出驚人的智慧，有時也會以一種極具迷惑性的方式給出錯誤結論。

而公理數學公司走的是一條融合之路。他們試圖兼收并蓄，既保留自然語言模型的直覺優(yōu)勢，又具備形式化驗證系統(tǒng)的嚴密邏輯。他們正在尋找這兩者之間的完美平衡點。這是一條最難走的路，因為它要求團隊同時精通兩個截然不同的學科領域。但與此同時，這也是一條通往真正超級智能的必經之路。

諸如Harmonic公司等其他初創(chuàng)企業(yè)，也在這場角逐中奮力追趕。該公司創(chuàng)始人表示，數學超級智能的誕生，正以分秒之勢不斷逼近。

白熱化的競爭格局

在一場學術研討會上，小野健受邀設計測試題，對這些新型人工智能模型進行評估。正是在這場研討會上，他真切感受到了這場競賽的緊迫感。“這就好比航海家出海前需要一張地圖。在啟程探索新大陸之前，你必須先明確自己的位置，以及哪些領域已經被前人探索過?！?小野健在談及模型測試基準的重要性時如此比喻。

參會之前，小野健曾信心滿滿地認為，自己的學術地位在未來數十年內都無可撼動。但參會之后，他所目睹的一切讓他深受震撼。他發(fā)現，在一些自己并不擅長的領域，人工智能模型的表現已經超越了他。從那以后，他每天晚上都會花上數小時，在手機上與這些模型進行對話交流?！拔遗c這些模型之間的領先優(yōu)勢正在不斷縮小。而在那些我并不精通的數學領域，我感覺自己已經被它們遠遠甩在了身后?！?小野健在接受《華爾街日報》采訪時，如此坦陳技術進步之迅猛帶來的沖擊。“就在那時，我豁然開朗。我意識到，這些模型正在為數學研究提供一種全新的范式?！?/p>

對于小野健及其家人而言，遷居硅谷是一次巨大的人生轉折。他打包好弗吉尼亞的家當，攜妻子與愛犬一同奔赴西海岸。他在公理數學公司擔任創(chuàng)始數學家一職 —— 這個頭銜是雙方幾經協商確定的，最初公司曾考慮過一個更為非正式的職位名稱。他的核心職責，是不斷挑戰(zhàn)這些人工智能模型的極限。他設計的測試題，只有真正理解數學原理的系統(tǒng)才能破解。他為那些構建人工智能核心算法的工程師們，提供了一張精準的 “導航地圖”。

小野健強調，自己做出這一決定絕非為了金錢。他早已是弗吉尼亞大學薪資最高的員工之一，并且拒絕了其他科技公司開出的更為優(yōu)厚的待遇。他之所以選擇跨界，是因為他渴望參與一項足以載入史冊的開創(chuàng)性事業(yè)。他想親眼見證，機器能否最終攻克那些困擾人類數百年的數學難題；他想知道，是否存在一個只有超級智能才能觸及的更深層次的真理維度。“作為一名純粹的數學家，我過去鮮有機會參與這種能真正改變世界運行方式的項目。如今，我有幸身處其中?！?小野健在一次談及加盟初創(chuàng)公司的采訪中說道。

公理數學公司位于帕洛阿爾托的辦公室，均以高斯、圖靈等數學與計算機科學巨匠的名字命名。盡管公司的掌舵人是一位24歲的年輕人，但小野健發(fā)現，身邊共事的許多人都與自己年齡相仿。在這個領域，許多頂尖研究者都已實現了經濟自由，他們有底氣去冒險追逐那些足以顛覆行業(yè)的偉大構想，渴望找到一個能定義自己職業(yè)生涯的終極項目。而對小野健來說，公理數學公司正是這樣一個項目。

“我從那些被我招募到公理數學的頂尖研究者和數學家口中聽到最多的一句話就是，攻克數學超級智能難題，將成為他們職業(yè)生涯中最輝煌的一筆遺產。” 洪樂潼在接受《商業(yè)內幕》Business Insider采訪時如此表示。

即便人工智能模型變得越來越智能，小野健依然堅信，總會有一些數學難題，始終無法被機器破解。在他看來，數學的疆域如此廣袤無垠，人類的直覺思維永遠有其不可替代的價值。但與此同時，他也滿懷期待，渴望見證機器能走多遠。他期待著第一臺人工智能數學家做出人類難以想象的重大發(fā)現的那一刻，更渴望成為助力這一時刻到來的推手。

“與人類不同，機器輔助的數學研究能夠打破學術專業(yè)壁壘，促進不同學科領域之間的思想交融?！?洪樂潼在與《神經元》雜志的討論中如此闡釋道。

當夕陽的余暉灑滿帕洛阿爾托的天空，公理數學公司的研發(fā)工作仍在緊鑼密鼓地進行著。服務器嗡嗡作響，黑板上寫滿了密密麻麻的方程式。小野健與洪樂潼并肩作戰(zhàn)，致力于打造一個既精妙嚴謹又強大高效的未來。

他們所做的，遠不止創(chuàng)辦一家公司那么簡單 —— 他們正在創(chuàng)造歷史。他們用實際行動證明，當經驗積淀的智慧與朝氣蓬勃的活力碰撞交融，一切皆有可能。

參考資料

https://www.youtube.com/watch?v=TV2MwcSkxp8

https://axiommath.ai

https://axiommath.ai/papers

小樂數學科普近期文章

·開放 · 友好 · 多元 · 普適 · 守拙·

讓數學

更加

易學易練

易教易研

易賞易玩

易見易得

易傳易及

歡迎評論、點贊、在看、在聽

收藏、分享、轉載、投稿

查看原始文章出處

點擊底部捐一筆

助力騰訊公益

點擊zzllrr小樂

公眾號主頁

右上角

置頂★加星

數學科普不迷路！