數(shù)學(xué)家安德魯·懷爾斯于1995年發(fā)表了費(fèi)馬大定理的證明。圖片來(lái)源：英國(guó)《自然》網(wǎng)站

　　費(fèi)馬大定理是過(guò)去半個(gè)世紀(jì)最著名的數(shù)學(xué)成果之一。9月4日，人工智能（AI）公司Anthropic宣布，其Claude模型僅用11天，就將英國(guó)數(shù)學(xué)家安德魯·懷爾斯1995年完成的費(fèi)馬大定理證明轉(zhuǎn)化為計(jì)算機(jī)可逐步驗(yàn)證的形式化證明。

　　“機(jī)器竟然能夠把人類(lèi)數(shù)學(xué)家的工作轉(zhuǎn)化為一份長(zhǎng)達(dá)1300萬(wàn)行、堅(jiān)不可摧的證明，這完全讓我震撼�！泵绹�(guó)羅格斯大學(xué)數(shù)論學(xué)家亞歷克斯·孔托羅維奇說(shuō)。

　　英國(guó)《自然》網(wǎng)站在7日發(fā)表的文章中稱(chēng)，這一成果表明，AI將在數(shù)學(xué)家的工作中發(fā)揮越來(lái)越重要的作用，不僅可幫助檢驗(yàn)數(shù)學(xué)證明，也可能參與產(chǎn)生新的數(shù)學(xué)推理。按照目前的發(fā)展速度，AI審查整個(gè)人類(lèi)數(shù)學(xué)知識(shí)庫(kù)，已不再是遙不可及的事，甚至可能發(fā)現(xiàn)一些廣為人知的數(shù)學(xué)結(jié)論中是否藏著錯(cuò)誤。而在兩年前，這還只是幻想。

　　AI打破人工核驗(yàn)局限

　　數(shù)學(xué)證明是一連串嚴(yán)密的邏輯步驟，只要其中一環(huán)出錯(cuò)，整個(gè)證明就可能坍塌。面對(duì)動(dòng)輒數(shù)百頁(yè)、涉及大量復(fù)雜理論的證明，單靠人工逐一核驗(yàn)每個(gè)環(huán)節(jié)，幾乎是不可能完成的任務(wù)。

　　費(fèi)馬大定理就是一個(gè)典型。1637年，法國(guó)數(shù)學(xué)家皮埃爾·德·費(fèi)馬提出了這個(gè)命題：當(dāng)整數(shù)n大于2時(shí)，不存在滿足xn+yn=zn的正整數(shù)x、y、z。

　　1908年，德國(guó)曾懸賞一筆獎(jiǎng)金（今天約合100萬(wàn)至200萬(wàn)美元），向數(shù)學(xué)家征集費(fèi)馬大定理的證明。僅第一年，就收到了621份證明，但沒(méi)有一份站得住腳。直到上世紀(jì)90年代，英國(guó)數(shù)學(xué)家安德魯·懷爾斯才真正攻克了這一難題。他在1995年5月發(fā)表了長(zhǎng)達(dá)129頁(yè)的證明，橫跨數(shù)論多個(gè)分支，匯集了大量現(xiàn)代數(shù)學(xué)成果。該證明通過(guò)了數(shù)學(xué)界審查并得到認(rèn)可，費(fèi)馬大定理就此塵埃落定。

　　所謂“形式化”證明，就是把數(shù)學(xué)證明翻譯成一種極其嚴(yán)格、精確的語(yǔ)言，讓計(jì)算機(jī)能夠自行驗(yàn)證其中的每一步，而不需要依賴(lài)人的主觀判斷。

　　近年來(lái)，AI進(jìn)行數(shù)學(xué)形式化的能力進(jìn)步很快。今年2月，AI輔助數(shù)學(xué)形式化取得一項(xiàng)里程碑式進(jìn)展，成功對(duì)菲爾茲獎(jiǎng)得主瑪麗娜·維亞佐夫斯卡關(guān)于8維和24維空間中最有效球體堆積方式的研究成果完成了計(jì)算機(jī)驗(yàn)證。不過(guò)，英國(guó)倫敦帝國(guó)理工學(xué)院數(shù)學(xué)家凱文·巴扎德說(shuō)，費(fèi)馬大定理的形式化工作“可能更困難一個(gè)數(shù)量級(jí)”。

　　預(yù)估十年工作量被AI壓縮到11天

　　2024年，巴扎德啟動(dòng)了一個(gè)項(xiàng)目，目標(biāo)是把懷爾斯的證明翻譯成Lean語(yǔ)言，以便計(jì)算機(jī)驗(yàn)證。他原本估計(jì)這項(xiàng)工作需要10年。項(xiàng)目自身的規(guī)劃文件就長(zhǎng)達(dá)86頁(yè)，資金支持目前已經(jīng)確定到2029年。

　　一年多后，AI大大推進(jìn)了工作進(jìn)度。Anthropic讓Claude承擔(dān)了費(fèi)馬大定理的形式化任務(wù)。據(jù)Anthropic介紹，哥倫比亞大學(xué)研究人員彭天翼及其團(tuán)隊(duì)讓數(shù)十個(gè)Claude智能體并行工作，不同智能體分別負(fù)責(zé)定義數(shù)學(xué)概念、證明較小的輔助定理，再將這些結(jié)果逐步組合起來(lái)。

　　Claude此次使用的Lean是一種專(zhuān)門(mén)用于形式化數(shù)學(xué)的證明輔助工具。數(shù)學(xué)家通過(guò)Lean把數(shù)學(xué)定義、定理和推理寫(xiě)成計(jì)算機(jī)能夠處理的形式，再由計(jì)算機(jī)檢查證明過(guò)程。

　　與Lean配套的Mathlib是一個(gè)由數(shù)學(xué)家持續(xù)維護(hù)的數(shù)學(xué)代碼庫(kù)，其中已經(jīng)收錄了大量經(jīng)過(guò)形式化處理的數(shù)學(xué)知識(shí)。新的數(shù)學(xué)證明可以調(diào)用其中已有的定義和定理，從而避免重復(fù)勞動(dòng)。

　　不過(guò)，這項(xiàng)工作最初并不順利。智能體會(huì)忘記其他智能體已經(jīng)完成的工作，產(chǎn)生重復(fù)工作，有時(shí)甚至停止協(xié)作。研究團(tuán)隊(duì)隨后使用Prove2Me工具，為智能體提供實(shí)時(shí)任務(wù)清單，記錄已完成和待辦事項(xiàng)，幫助各智能體調(diào)用已有成果。

　　經(jīng)過(guò)11天運(yùn)轉(zhuǎn)，Claude完成了整個(gè)形式化過(guò)程，證明了約3萬(wàn)個(gè)輔助定理，生成了約1300萬(wàn)行代碼，規(guī)模相當(dāng)于160部長(zhǎng)篇小說(shuō)。

　　正確判定率從99.9%到100%

　　經(jīng)過(guò)形式化之后，懷爾斯的證明獲得了一份計(jì)算機(jī)可逐行核驗(yàn)的“認(rèn)證”。巴扎德說(shuō)，過(guò)去自己有“99.9%的把握”認(rèn)為這份證明正確，如今則是“100%”。

　　這種確定性對(duì)于數(shù)學(xué)同行評(píng)審尤為關(guān)鍵。數(shù)學(xué)論文數(shù)量不斷增加，篇幅越來(lái)越長(zhǎng)，涉及的數(shù)學(xué)知識(shí)也愈加復(fù)雜，人工檢查一份完整證明往往需要耗費(fèi)大量時(shí)間。即使如此，仍可能漏掉一些錯(cuò)誤。

　　數(shù)學(xué)家對(duì)這種情況并不陌生。開(kāi)普勒猜想的一項(xiàng)計(jì)算機(jī)輔助證明花了4年時(shí)間，之后審查小組仍只能給出“99%確定”的評(píng)價(jià)。格里戈里·佩雷爾曼關(guān)于龐加萊猜想的證明，也花費(fèi)了大約4年時(shí)間才得到數(shù)學(xué)界充分理解和認(rèn)可。

　　美國(guó)加州大學(xué)圣迭戈分校數(shù)學(xué)家弗雷德里克·曼納斯設(shè)想，如果有一種“魔法”，能夠把一篇發(fā)表在預(yù)印本平臺(tái)arXiv上的論文交給機(jī)器，由機(jī)器判定證明是否正確，或者直接指出其中錯(cuò)誤，那將具有極其重要的價(jià)值。

　　如今，Claude生成的約1300萬(wàn)行證明已經(jīng)公開(kāi)在GitHub上，任何數(shù)學(xué)家都可以免費(fèi)獲取并逐行核查。隨著AI參與數(shù)學(xué)形式化的能力不斷提升，曼納斯設(shè)想的“魔法”正從想象一步步走向現(xiàn)實(shí)。（記者 張佳欣）