科學人/AI首次獨立破解30年數學懸案!人類數學家最終堡壘已被攻克?

圖/Gemini生成
圖/Gemini生成

在甫出刊的《科學人》雜誌2025年12月號【專家看新聞】中,美國約翰霍普金斯大學數學家里爾(Emily Riehl)才撰文指出她不擔心自己會因AI失業。里爾在文中強調,就算頂尖人工智慧(AI)模型在國際數學奧林匹亞(IMO)會外賽取得金牌級成績,但數學更重視經得起邏輯檢驗的「形式證明」(formal proof)。她認為,大型語言模型(LLM)在基本問題上會犯錯,而或使用形式化語言運作的電腦證明助手,想達到形式驗證的標準並嘗試解答她鑽研的數學問題「還有很長一段路要走」。然而,AI圈一天,人間十年,她的看法在前幾天竟遭最新AI模型打臉,因為一樁懸宕數十年的數學懸案竟被具備形式證明能力的AI獨立攻克了。

數學界的怪傑:漂泊的艾狄胥

要理解這項突破的份量,必須先認識匈牙利數學家艾狄胥(Paul Erdős)。他是20世紀最多產的數學家之一,一生發表了約1500篇論文,無人能出其右。艾狄胥生活灑脫,沒有結婚、沒有固定工作、沒有房子,只帶著一個裝著衣物和筆記本的行李箱周遊世界。他將數學視為一種社會活動,會出現在同事家門口,敲門宣布「我的大腦敞開了」(my brain is open),然後走進去和數學家進行一場激烈的腦力激盪。

提出上千問題的匈牙利傳奇數學家艾狄胥(Paul Erdős,1913-1996)圖/取自Kmhkmh@WIKI
提出上千問題的匈牙利傳奇數學家艾狄胥(Paul Erdős,1913-1996)圖/取自Kmhkmh@WIKI

艾狄胥是公認的「問題提出者」,一生中提出了至少上千個未解決的猜想,即「艾狄胥問題」(Erdős’s problems)。他針對這些問題懸賞獎金,金額從25美元到難度最高的10000美元不等,解決艾狄胥問題一直被數學界視為重大成就。

從人機接力到AI獨挑大樑

近期,艾狄胥問題網成了見證AI突破的舞台。首先登場的是艾狄胥問題#367的「人機接力賽」。數學家范多恩(Wouter van Doorn)提出了反證的「直覺」(vibe),但論證依賴於一個特定的同餘恆等式。菲爾茲獎得主陶哲軒(Terence Tao)接力,將恆等式丟給Google最近火熱的AI模型Gemini「深度思考模式」(Deep Think)。結果,AI在10分鐘內就完成了原本可能要花上人類數學家好幾天的繁瑣運算驗證。

隨後,陶哲軒介入,將AI過於複雜的證明轉譯成人類可讀的版本。最後一棒由數學家阿列克謝夫(Boris Alexeev)使用Harmonic公司的AI工具「亞里斯多德」(Aristotle),僅花兩三個小時就完成了將證明轉化為Lean語言,順利達成所謂的形式化,並仔細檢查是否有任何幻覺和AI取巧(AI exploits),結論是他們否證了#367的第二部份(並未完全解決此問題)。

這種人機協作已經是數學研究上的大突破,但才過幾天,Harmonic公司就高調宣布亞里斯多德這次 「獨自」證明了艾狄胥問題#124。這是一個懸宕了近30年的數論猜想。AI不僅攻克證明,更直接用Lean語言完成形式化驗證,確保了邏輯的百分之百正確性。

網站維護者、英國皇家協會大學研究員布魯姆(Thomas F. Bloom)雖然肯定AI在無人干預下完成形式化令人印象深刻,但也指出AI所提出的#124解答相對容易且簡短,有可能已出現在訓練資料中。但台灣AI趨勢專家蕭上農(Fox)強調,AI能夠自主定位並形式化這個數學懸案的較弱版本,已是種巨大的飛躍,且從#367的輔助到#124的獨挑大樑,AI進化速度令人咋舌。

「直覺證明」時代來臨:數學家不會失業而是成為指揮官

Harmonic公司創辦人泰內夫(Vlad Tenev)高調宣示:「直覺證明」(vibe proving)的時代已來臨。他認為,這印證了陶哲軒的預言:未來的數學研究,人類將負責提供「直覺與猜想」,而AI則負責處理那些嚴謹、繁瑣的形式化證明過程,陶哲軒稱之為直覺形式化(vibe formalizing)。

陶哲軒發文表示,即使這類AI集中解決的是數學長尾問題(long tail)中相對容易的「最低的果實」,也表明AI已來到原創數學研究的門口,這些工具日益增強的能力,將協助人類研究者清除最容易解決的問題,將真正困難的題目標記出來。

這項突破可能為數學界帶來巨大的典範轉移,過去,數學家是建築工人,要親手搬每一塊磚(撰寫證明細節)。未來的數學家將轉職為建築師,負責畫出藍圖(提供高階直覺),而AI負責砌磚(形式化驗證),這將讓數學研究以更快的速度向前邁進。

資料來源

1.Robinhood CEO Vlad Tenev's Math AI Startup Claims To Have Solved An Erdos Problem That Was Open For 30 Years

2.蕭上農,〈數學接力:陶哲軒、直覺與 AI 的協作展示〉

3.蕭上農,陶哲軒預言成真?AI 剛剛「獨自」解開了 30 年前的數學難題

4.陶哲軒,自動化:數學長尾問題的清場

5.Paul Erdős - Wikipedia

(本文出自2025.12.01《科學人》網站,未經同意禁止轉載。)

AI 科學人雜誌

相關新聞

新聞中的公民與社會/中東戰火釀危機…避免輸入性通膨 該採取何種貨幣政策

中東戰事造成國際油價居高不下,引發國內通貨膨脹升溫與經濟成長的疑慮。中央銀行總裁楊金龍表示,如果全年平均油價上漲到每桶一百美元,消費者物價指數(CPI)年增率恐怕要調升到百分之一點九。但他也說…

紐時賞析/北極暖化  毒水染紅阿拉斯加河川

Record-setting temperatures and rainfall in the Arctic over the past year sped up the melting of permafrost and washed toxic minerals into more than 200 rivers across northern Alaska, threatening vital salmon runs, according to a report card issued by federal scientists.

丹鳳閱讀很「天下」 AI時代,你是駕駛還是乘客?

新北市立丹鳳高級中學圖書館為慶祝即將到來的世界閱讀日,特邀《天下雜誌》教育媒體團隊進校,以「AI時代,你是駕駛還是乘客?」為題舉辦對談活動…

好讀周報/美通訊巨頭大規模斷訊!百萬人「無手機可用」數小時爆焦慮

威訊(Verizon)、AT&T和T-Mobile名列美國三大科技電信公司,就如同台灣電信三雄中華電信、台灣大哥大和遠傳電信一般,戮力以無遠弗屆的電信網路設施,守護著普羅大眾的日常通訊需求。

寫作教室/抓住題目核心本質!師指導「3招切題」 連結思考與表達的橋

「老師,我真的有努力寫了,但分數還是很低……」考後幾天,一位學生低聲對我說。

紐時賞析/在Instacart買雜貨 同品不同價

On a Thursday in early September, more than 40 strangers logged in to Instacart, the grocery-shopping app, to buy eggs and test a hypothesis.

udn討論區

0 則留言
規範
  • 張貼文章或下標籤,不得有違法或侵害他人權益之言論,違者應自負法律責任。
  • 對於明知不實或過度情緒謾罵之言論,經網友檢舉或本網站發現,聯合新聞網有權逕予刪除文章、停權或解除會員資格。不同意上述規範者,請勿張貼文章。
  • 對於無意義、與本文無關、明知不實、謾罵之標籤,聯合新聞網有權逕予刪除標籤、停權或解除會員資格。不同意上述規範者,請勿下標籤。
  • 凡「暱稱」涉及謾罵、髒話穢言、侵害他人權利,聯合新聞網有權逕予刪除發言文章、停權或解除會員資格。不同意上述規範者,請勿張貼文章。