數學學術界近日迎來了一場技術地震。初創AI公司Axiom Math對外宣佈,其自主研發的AI系統自今年 2 月以來提交的 8 篇數學論文中,已有 5 篇正式通過同行評審並被學術期刊接收。這一突破不僅展示了人工智能在純數學研究領域的巨大潛力,更標誌着AI在解決高難度複雜學術猜想上邁出了實質性的一步。
在這批被接收的論文中,一項關於分拆多項式倒數和(Reciprocals of Partition Polynomials)的研究成果尤爲引人矚目。該研究直接瞄準了學界長期存在的 10 個核心猜想,AI系統不僅成功證明了其中的 6 個,甚至還敏銳地發現了原始命題中的一個反例。與以往只會用自然語言撰寫“似是而非”證明的大模型不同,該團隊研發的AxiomProver系統開創了全新的工作流:它能將自然語言表達的數學問題精確翻譯爲Lean形式化證明,並由獨立的檢測器對每一步邏輯進行嚴密驗證。這種“機器證明、機器檢查、人類數學家潤色解釋”的人機協作模式,從根本上杜絕了AI的“邏輯幻覺”。
而這一硬核科技成果的幕後推手,是一位年僅 25 歲的中國姑娘。Axiom Math的創始人洪樂潼 2001 年出生於廣州,自幼便展露出驚人的數學天賦。她 17 歲考入麻省理工學院(MIT),僅用三年時間便斬獲數學與物理雙學位,並在本科期間發表了 9 篇論文。在相繼拿下牛津大學碩士以及斯坦福大學法學與數學雙博士錄取資格後,她毅然決定於 2024 年秋季從斯坦福退學,全職投入創業。
洪樂潼的硬核背景和可驗證AI的宏大願景,吸引了頂級人才與資本的瘋狂涌入。前Meta AI專家Shubho Sengupta以及知名數學家Ken Ono(小野健)相繼加入成爲其創業合夥人,後者甚至爲此辭去了弗吉尼亞大學的終身教職。在不到一年的時間裏,Axiom Math便完成了兩輪共計2. 64 億美元(約合 14 億元人民幣)的融資,公司估值直接飆升至 16 億美元。
據瞭解,AxiomProver在此前就已經在普特南數學競賽中拿下滿分,並攻克了困擾學術界數十年的兩個埃爾德什(Erdős)猜想。然而,洪樂潼和團隊的野心遠不止於“AI數學家”,他們的最新研究已經跨界至博弈論與經濟學領域。該團隊正致力於將這種“生成、形式化、驗證”的閉環推理能力,推向其他高風險、高精度要求的決策場景,打造一個能夠自我改進的超級智能推理器。
