數(shù)學(xué)家小野健（Ken Ono）和他的學(xué)生洪樂潼，圖片來源：WSJ
最近，美國一位傳奇數(shù)學(xué)家，放下了終身教職，開始為一位24歲的年輕人“打工”。
據(jù)《華爾街日報(bào)》，57歲的美國頂尖數(shù)學(xué)家小野?。↘en Ono）辭去了弗吉尼亞大學(xué)終身教職，上周正式加入了他之前的學(xué)生，一位24歲年輕人洪樂潼（Carina Hong）創(chuàng)辦的AI數(shù)學(xué)公司Axiom Math，成為第15號員工。
小野健出生于1968年，是美國頂尖數(shù)論學(xué)家，弗吉尼亞大學(xué)終身教授，研究領(lǐng)域?yàn)閿?shù)論（ number theory），曾任弗吉尼亞大學(xué)教務(wù)長STEM顧問。
當(dāng)然，洪樂潼亦是一位數(shù)學(xué)界的“天才少女”。她用三年時間從麻省理工學(xué)院畢業(yè)，作為美國頂尖的本科數(shù)學(xué)研究者榮獲摩根獎（Morgan Prize），并獲得羅德獎學(xué)金（Rhodes scholarship）。
之后，她前往斯坦福大學(xué)攻讀法律和數(shù)學(xué)雙博士學(xué)位。中途，她決定退學(xué)創(chuàng)辦Axiom Math，并完成了6400萬美元的融資，從Meta挖來數(shù)名AI研究員，以及，請來了她的導(dǎo)師。
小野健的決定，在數(shù)學(xué)界與AI圈都引起廣泛關(guān)注，因?yàn)檫@是少有的頂尖純數(shù)學(xué)家轉(zhuǎn)身投入AI創(chuàng)業(yè)公司的案例，也意味著“數(shù)學(xué)研究+AI”有了一種新方向。
兩年前，22歲的洪樂潼在硅谷創(chuàng)辦了Axiom Math，目標(biāo)是打造“AI數(shù)學(xué)家”：一種AI系統(tǒng)能夠像人類數(shù)學(xué)家那樣推理、發(fā)現(xiàn)、并證明數(shù)學(xué)定理。
Axiom Math成立后不久便完成了6400萬美元的種子輪融資，由B Capital領(lǐng)投，Greycroft，Madrona Venture Group和Menlo Ventures參投，融資后公司估值達(dá)到3億美元。
在Axiom Math官網(wǎng)，有一則頗令人心潮澎湃的使命宣言：
數(shù)學(xué)發(fā)現(xiàn)使我們能夠理解從人腦到宇宙的每一個復(fù)雜系統(tǒng)?？v觀人類歷史，每一種數(shù)學(xué)工具都極大地?cái)U(kuò)展和加快了后續(xù)發(fā)現(xiàn)的規(guī)模和速度。
人工智能正處于一個歷史性的轉(zhuǎn)折點(diǎn)：數(shù)學(xué)發(fā)現(xiàn)可以以指數(shù)級規(guī)模和令人振奮的速度展開。我們正站在數(shù)學(xué)復(fù)興的門檻上。
這場復(fù)興建立在三大支柱之上：人工智能、編程語言和數(shù)學(xué)。數(shù)學(xué)家與人工智能的合作，以前所未有的規(guī)模和速度創(chuàng)造出新的想法。編程語言將抽象概念轉(zhuǎn)化為可驗(yàn)證的現(xiàn)實(shí)。它們共同創(chuàng)造了一個發(fā)現(xiàn)的飛輪：每一次突破都加速著下一次的到來。
我們正在組建一支首次在所有三個領(lǐng)域都擁有精湛技藝的團(tuán)隊(duì)。他們是利用人工智能打破曾經(jīng)難以逾越的障礙的先驅(qū)者：大規(guī)模同步訓(xùn)練的架構(gòu)師、將人工智能引入代碼生成的遠(yuǎn)見卓識者，以及運(yùn)用Transformer解決百年數(shù)學(xué)猜想的開拓者。
數(shù)學(xué)發(fā)現(xiàn)的未來從這里開始。
洪樂潼本人一直對數(shù)學(xué)發(fā)現(xiàn)抱有極大興趣。她發(fā)現(xiàn)，奧數(shù)帶來的是持續(xù)的多巴胺刺激，而研究型數(shù)學(xué)更像是“拿頭撞墻”的過程，這是一種痛苦與磨礪，而她正喜歡這點(diǎn)。
Axiom Math的研究方向，包括大模型形式化定理證明、合成數(shù)學(xué)數(shù)據(jù)生成、猜想自動提出與驗(yàn)證，以及面向芯片設(shè)計(jì)、物流優(yōu)化、金融系統(tǒng)的高階算法自動發(fā)現(xiàn)。
創(chuàng)業(yè)僅4個月，洪樂潼帶領(lǐng)不足10人的團(tuán)隊(duì)（核心成員僅4人），用自主研發(fā)的Axiom Prover系統(tǒng)，可在分鐘級完成IMO銀牌難度幾何題，并接連攻克兩道懸而未決的數(shù)學(xué)難題，震驚數(shù)學(xué)界與AI圈：
這兩項(xiàng)突破的核心優(yōu)勢的是“形式化驗(yàn)證”——通過Lean編程語言將數(shù)學(xué)證明轉(zhuǎn)化為可執(zhí)行程序，確保結(jié)果100%可信，而這正是洪樂潼結(jié)合數(shù)學(xué)研究與AI技術(shù)的創(chuàng)新之處，也讓Axiom快速拉開與巨頭的差距。
公司對外宣稱不以“替代數(shù)學(xué)家”為終點(diǎn)，而是構(gòu)建“人機(jī)共寫”的新一代數(shù)學(xué)基礎(chǔ)設(shè)施：讓模型負(fù)責(zé)窮舉與形式化，數(shù)學(xué)家負(fù)責(zé)直覺與價值判斷，從而把平均發(fā)現(xiàn)周期縮短一個數(shù)量級。
Axiom Math的商業(yè)路線采取“底層模型+垂直SaaS”雙輪模式，前期主要加速開發(fā) “AI數(shù)學(xué)家”，針對benchmark 問題 (數(shù)學(xué)、算法、物理、加密) 測試與優(yōu)化。
引擎成熟后，會推出給企業(yè)和機(jī)構(gòu)的SaaS/API產(chǎn)品，主攻量化金融、風(fēng)險管理、芯片/硬件驗(yàn)證、科研/R&D流程等領(lǐng)域。
小野健在Axiom Math的日常工作包括：給AI模型設(shè)計(jì)必須通過的數(shù)學(xué)難題，構(gòu)建數(shù)學(xué)能力的基準(zhǔn)測試，推動模型向“數(shù)學(xué)創(chuàng)造力”進(jìn)化等。
作為數(shù)學(xué)巨人的另一面，小野健是極度“搖滾”，是“老頑童”。
2007年，《紐約時報(bào)》曾發(fā)表了一篇人物特寫The Man Who Makes Math Rock（《這個讓數(shù)學(xué)搖滾的人》），描述小野健在講臺上“像吉他手一樣來回奔跑、用幻燈機(jī)打出爆炸式彩色公式”，并把他的演講比作“數(shù)學(xué)演唱會”。后來，他還上過好萊塢啤酒廣告，被ESPN稱為“最會彈吉他的數(shù)學(xué)家”。
這種特立獨(dú)行的行事風(fēng)格，也難怪小野健從頂尖學(xué)府離職，加入年輕學(xué)生創(chuàng)辦的新公司。
事實(shí)上，AI對于數(shù)學(xué)的影響遠(yuǎn)早于大眾對于AI的理解。
1956年出現(xiàn)的“第一個人工智能程序”——Logic Theorist，證明了數(shù)學(xué)家阿弗烈·諾斯·懷特海（Alfred North Whitehead）和伯特蘭·羅素（Bertrand Russell）的《數(shù)學(xué)原理》（Principia Mathematica）第二章中前52個定理中的38個，并為其中一些定理找到了新的、更簡潔的證明。
2024年，DeepMind與紐約大學(xué)推出了一套名為Alpha Geometry的AI系統(tǒng)。該系統(tǒng)通過合成了約1億條幾何定理與證明作為訓(xùn)練數(shù)據(jù)，從零開始訓(xùn)練，沒有人類示范。它在一個包含30道IMO-style幾何題的測試集中，解出了25道。這個成績非常接近過去人類IMO金牌選手在這些題目上的平均水平，被視為AI在復(fù)雜邏輯推理與數(shù)學(xué)證明方面的重要里程碑。
如果說1956年AI僅能證明人類已驗(yàn)證的理論，那么，到了2025年，AI已經(jīng)可以接過教授的筆，并告訴他，“這個問題其實(shí)沒那么難”。
AI數(shù)學(xué)已經(jīng)在自主質(zhì)疑和驗(yàn)證人類頂級數(shù)學(xué)家數(shù)百年來建立的學(xué)術(shù)成果，也難怪?jǐn)?shù)學(xué)巨人也會對自己的身份認(rèn)同產(chǎn)生動搖。
而小野健就曾一度對外這樣自我介紹，“我是NI，天生智能（Naturally intelligent）”。
與AI與數(shù)學(xué)的歷史刻度同步變得緊湊的，還有近年來全球頂尖科學(xué)家“棄研從創(chuàng)”的密度。
今年，美國國家工程院院士、美國國家醫(yī)學(xué)院院士、美國藝術(shù)與科學(xué)院院士，美國斯坦福大學(xué)主要紅杉講授教授李飛飛創(chuàng)辦了World Labs，專注世界模型（World Model）。
最近，AI教父級人物、圖靈獎得主楊立昆（Yann LeCun）離職Meta，將創(chuàng)辦一家專注于先進(jìn)機(jī)器智能研究項(xiàng)目（AMI）的初創(chuàng)公司。
在中國也出現(xiàn)類似潮流。2016年，香港科技大學(xué)自動化技術(shù)中心主任李澤湘教授離開教研一線，全力孵化創(chuàng)新生態(tài)，成功投資孵化了大疆創(chuàng)新、云鯨智能等硬科技企業(yè)。
同樣，在2016年，中國科學(xué)技術(shù)大學(xué)少年班數(shù)學(xué)與應(yīng)用數(shù)學(xué)專業(yè)、中國科學(xué)技術(shù)大學(xué)計(jì)算機(jī)學(xué)院攻讀博士陳天石，帶領(lǐng)團(tuán)隊(duì)創(chuàng)立寒武紀(jì)，2025年，寒武紀(jì)以6643億市值登頂A股“股王”。
事實(shí)上，教授跳槽進(jìn)創(chuàng)業(yè)公司，并不是AI時代才有的新鮮事，自20世紀(jì)60年代硅谷形成“科技-資本-高校”三角生態(tài)以來，幾乎每一次技術(shù)范式的更替，象牙塔里最稀缺的“大腦”都會被新興產(chǎn)業(yè)“吸走”。
資本需要學(xué)術(shù)權(quán)威背書，而高校隨即以“停薪留職、專利分成、創(chuàng)業(yè)休學(xué)”等制度降低機(jī)會成本，讓教授跳槽成為“進(jìn)可攻、退可守”的抉擇。對高校來說，頂尖學(xué)者涌向產(chǎn)業(yè)，最直接的影響卻是學(xué)校研究能力的斷檔。
科學(xué)家創(chuàng)業(yè)遷徙潮的另一面，會直接導(dǎo)致高校頂會論文的出稿率下滑，同步拉低基礎(chǔ)科研經(jīng)費(fèi)，還會導(dǎo)致與關(guān)鍵學(xué)者有關(guān)的交叉學(xué)科萎縮。
不過，走出校園的頂尖“大腦”也并未切斷與母校的聯(lián)系，大多數(shù)成功的頂級學(xué)者都會以捐贈、兼職、公開課持續(xù)回流。
每一次頂級學(xué)者的人才外溢，都伴隨著學(xué)科話語權(quán)大遷移。在學(xué)術(shù)圈常有人說，半導(dǎo)體看斯坦福與伯克利的電機(jī)系，生物醫(yī)藥看UCSF與哈佛醫(yī)學(xué)院，互聯(lián)網(wǎng)看斯坦福與卡內(nèi)基梅隆的CS。而當(dāng)今的AI，則是由卡內(nèi)基梅隆大學(xué)（CMU）引領(lǐng)，與麻省理工、斯坦福、伯克利等頂尖院校共同驅(qū)動的格局。
在這前沿技術(shù)潮起潮落之間，那些未能及時做出反應(yīng)的院系或者人才，命運(yùn)也會隨之起起落落。（作者｜陶天宇，編輯｜李程程）
快報(bào)
根據(jù)《網(wǎng)絡(luò)安全法》實(shí)名制要求，請綁定手機(jī)號后發(fā)表評論
高校論文出稿率下滑，會不會影響學(xué)科排名？這連鎖反應(yīng)也太嚇人了！
小野健去 Axiom Math，會不會把自己的人脈和資源帶過去？幫公司更快發(fā)展！
數(shù)學(xué)家都去搞 AI 創(chuàng)業(yè)了，以后高校數(shù)學(xué)研究不得靠年輕學(xué)者撐著？
高校研究能力要斷檔了，頂尖學(xué)者都走了，論文出稿率不得往下掉？
小野健去 Axiom Math，說不定是想讓 AI 幫數(shù)學(xué)研究提速，這想法挺超前！
Axiom Math 才成立 4 個月就攻克兩道數(shù)學(xué)難題，這 “AI 數(shù)學(xué)家” 進(jìn)度也太快了吧！
小野健加入后，Axiom Math 的研究實(shí)力又上一層，以后出成果會更頻繁吧！
小野健從弗吉尼亞大學(xué)辭職，放著鐵飯碗不要，對創(chuàng)業(yè)也太有信心了！
Axiom Math 拿 6400 萬融資，資本這么看好 “數(shù)學(xué) + AI”，這賽道要火了？
AI 讓數(shù)學(xué)研究效率翻倍，難怪頂尖學(xué)者都想離開高校，去創(chuàng)業(yè)公司搞突破！