8篇由同一個系統生成或形式化證明的數學論文
夢晨 發自 凹非寺
量子位 | 公眾號 QbitAI
數學論文預印本里，悄悄混進了8篇AI作品。
更準確地說，是8篇由同一個系統生成或形式化證明的數學論文。
初創公司Axiom Math宣佈，他們從2026年2月開始提交的8篇論文，到5月28日有5篇已經通過同行評審，登上學術期刊。。
創始人洪樂潼，2001年出生於廣州，本科MIT三年拿下數學與物理雙學位，還拿過北美數學本科生的最高榮譽羅德獎學金和摩根獎。
在斯坦福讀博期間，她退學了。
退學的理由正是創辦Axiom Math。
Axiom在3月完成2億美元（約13.56億元人民幣）融資，估值16億美元（約108.46元人民幣）。
這批提交的論文橫跨數論、組合、交換代數、代數幾何/幾何動力系統、表示論和Dyck path模型。
AI證明，機器檢查，人類審稿
要理解Axiom Math做的是什麼，這8篇論文是最好的切入點。
其中一篇Reciprocals of Partition Polynomials，已被Annals of Acad. Rom. Sci.接收。
這篇論文研究的是由partition subsum polynomials構造出reciprocal sums，目標是處理Ballantine、Beck、Feigon和 Maurischat 提出的10個猜想。
AI證明了其中6個，還發現了一個原始命題裡的反例。
這個AI系統交AxiomProver ，產生的論文真沒有停在自然語言，而是生成形式化證明。
大模型可以寫出很像證明的文字。
但問題在於，自然語言證明再順滑，也可能藏著邏輯縫隙。讀者、審稿人和作者都要靠理解去判斷哪裏站得住。
AxiomProver換了一種交付方式：
研究者給出自然語言問題陳述，系統把問題翻譯成Lean形式化證明。完成後，再由單獨的檢測器驗證每一步。
論文的文字仍然由人類數學家會把形式化證明配上學術解釋。
在這個實驗中，AI沒有代替人類，而是實踐了一種新的人機協作模式。
AI負責生成或形式化可檢查證明，人類數學家負責問題表達、論文解釋和審稿溝通。
Axiom的創始數學家Ken Ono（小野健）表示，在某些情況下，系統被給定開放研究問題。會在大約 24 小時內生成完整、機器驗證的證明。
00後華人創辦，佈局可驗證AI
創始人洪樂潼，她自幼便展現出非凡的數學天賦，並在父母的支援下投身於數學競賽。
14歲時，她便在草稿紙上寫下「MIT」以激勵自己。
高中時期，她就讀於華南師範大學附屬中學，進入廣東省數學奧林匹克省隊，在多項全國數學競賽中獲獎。
2019年，17歲的洪樂潼考入MIT，僅用三年時間便完成了數學與物理雙學位的學業，本科期間就發表了9篇學術論文。
本科畢業後，她赴牛津大學攻讀神經科學碩士學位，再次旗艦接觸了人工智慧和機器學習研究。
隨後她被斯坦福大學的數學博士和法學博士雙學位錄取。
爲了全身心投入創業，她於2024年秋季從斯坦福大學退學。
她的創業合作伙伴Shubho Sengupta也從Meta辭職，兩人從AI與數學推理的交叉可能性出發，決心解決AI的幻覺問題。
後來知名數學家Ken Ono為此辭去了弗吉尼亞大學的終身教職，全職加入。
AxiomProver在普特南數學競賽拿下滿分，還解決了兩個困擾學界數十年的Erdős猜想。
但「AI數學家」只是Axiom Math的第一步，他們的願景是打造一個能夠自我改進的超級智慧推理器。
不到一年，Axiom完成了6400萬美元種子輪和2億美元A輪融資，估值飆到16億美元。
投資人Matt Kraning如此評價這家公司：「AI將編寫所有程式碼，但數學將證明其是否有效。」。
如果一個 AI 系統能把數學證明交給機器逐步檢查，那麼同樣的「生成、形式化、驗證」閉環，也可能被拿去處理其他學科，以及高風險決策場景。
5月27日，Axiom提交的最新一篇論文就跨界到了博弈論和經濟學領域。
與哈佛商學院教授Scott Duke Kominers合作，用Lean形式化證明Robert Aumann的經典定理。
洪樂潼曾說創業者要選最難的問題，甚至需要5到10年才能解決的那種。
現在看起來，她選的這條路同樣也是最被關注的之一。
參考連結：
[1]
https://x.com/axiommathai/status/2059640254341284320
[2]
https://axiommath.ai/papers