AI攻克費馬大定理？數學家放棄5年職業生涯，將100頁證明變代碼

新智元報道

編輯：Aeneas 好睏

【新智元導讀】困擾全世界幾個世紀的「臭名昭著」謎題——費馬大定理，或將被AI攻克？一位英國數學家宣佈，即將啓動用Lean重現費馬大定理證明過程的項目，將100頁證明變成代碼。從此，世界頂尖數學難題的證明將成爲「衆包」項目，你我都可以進去添幾筆。

費馬大定理，即將被AI攻克？

而且整件事最意味深長的地方在於，AI即將解決的費馬大定理，正是爲了證明AI無用。

曾經，數學屬於純粹的人類智力王國；如今，這片疆土正被先進的算法所破譯，所踐踏。

費馬大定理，是一個「臭名昭著」的謎題，在幾個世紀以來，一直困擾着數學家們。

它在1993年被證明，而現在，數學家們有一個偉大計劃：用計算機把證明過程重現。

他們希望在這個版本的證明中，如果有任何邏輯上的錯誤，都可由計算機檢查出來。

項目地址：https://github.com/riccardobrasca/flt3

3月底，數學家Pietro Monticone激動地表示，自己和同事幾乎在leanprover中完成了指數3的費馬大定理的形式化。

他們會盡快把形式化過程移植到Mathlib中，以便在FLT項目中使用。

證明過程大致遵循Wiles的證明，但會略有改動。

用Lean把費馬大定理變成代碼

當四月到來時，數學家兼程序員Kevin Buzzard將發佈這個計劃：通過計算機代碼，完成費馬大定理的證明。

項目在4月上線後，公開的藍圖就會出現在網上，屆時，Lean社區的任何人，都可以爲形式化證明做出自己的貢獻。

把一個開創性的100頁數學證明，變成計算機代碼，這個過程容易實現嗎？

這當然就要歸功於被陶哲軒大加讚賞、沉迷使用的證明工具Lean，它可以讓用戶把散文式的證明轉化爲用於測試的規則和邏輯。

但無論如何，這項工程都不簡單，預計將歷時多年，而Kevin Buzzard頁獲得了項目的資金支持。

大家都明白，這個項目，很可能是迄今爲止最複雜的計算機化方式證明之一。

費馬大定理

費馬大定理，堪稱是史上最精彩的一個數學謎題。

而證明費馬大定理的過程，直接就是一部數學史。

我們耳熟能詳的費馬大定理，由17世紀的法國數學家皮埃爾·德·費馬提出。遺憾的是，他未能在有生之年找到證明。

於是，這項起源於三百多年前的難題，直接挑戰了人類整整3個世紀，多次震驚全世界，耗盡人類衆多最傑出大腦的精力，也讓千千萬萬業餘者癡迷。

這個定理聲稱，不存在三個正整數a、b、c能滿足方程 (a^n + b^n = c^n)，其中n是任何大於2的整數。

這個證明的難點就在於，數學家很難找出一個否定案例：我們怎麼能保證一定不存在這樣一個無窮大的整數n，能滿足這個方程式呢？

幸好，對於今天的數學家來說，將無窮大的概念轉換成邏輯，並不是什麼新鮮事了。

在較爲簡單的證明中，我們可以依靠歸納法——

一旦某個邏輯對某個數字成立（比如8），那麼它對於之後的每一個數（比如9、10、11等）都同樣成立，直到無限大。

然而，費馬大定理卻是數學界百年來的一塊絆腳石。

直到1993年，英國數學家Andrew Wiles用一份長達100頁的書面證明，解開了這一謎團。

計算機爲什麼無法證明費馬大定理？

業界認爲原因有三：

1. 計算機無法推導出無窮種

2. 計算機無法證明邏輯正確

3. 計算機可能會出現轉瞬即逝的失誤

幸好有Lean輔助證明

一份100頁的數學證明，無論是對於普通的數學系學生，還是數學家，都不是那麼好駕馭的。

好在，我們可以不再依賴傳統的證明方法，可以求助於Lean這樣的工具。

它是一款基於C++開發的編程工具，專爲編寫和驗證歸納法證明而設計。

如今許多所謂的「人工智能」，不過是巧妙地排列模仿人類語言的文字。但Lean這類計算機輔助的證明，更深入地融合了人類的思維方式，和計算機輔助加強的能力。

Lean編程工具，進入本科課堂

在倫敦帝國理工學院教數學的Kevin Buzzard，花費了數年時間，利用Lean爲學院的整個本科數學課程開發了支持工具。

通過這些工具，學生們可以將課堂上討論的內容分解成邏輯和數學運算的步驟。

這就彷彿是一個數學證明上的羅塞塔石碑。

同爲數學教師的Clarissa Littler，就非常贊同Kevin Buzzard的理念。

她在波特蘭社區學院教授離散數學。過去兩個學期裡，她都在離散數學課上用Kevin Buzzard開發的「Lean經典入門遊戲」。

地址：https://adam.math.hhu.de/

她會用「自然數博弈」，幫學生熟悉數學歸納法的思想，通過「集合論博弈」，讓他們習慣於對集合進行推理。

在這個過程中，學生們對「嚴格遵循邏輯規則編寫證明」，和「用通俗語言解釋事物真理」之間的理解差距，就會逐漸彌合。

Littler強調，課程的一大重點，就是讓數學基礎不太牢固的學生，更自如地用數學家的方式思考，同時更好地理解證明、證據和展示真理的方法。

這種從形式邏輯到規則列表，再到用散文表達的轉變，是將項目分解成互相協作的代碼片段的關鍵所在。

而這一點，在編程和純數學的交叉領域尤爲重要，也正是Lean這樣的工具能大放異彩的地方。

Buzzard表示，他希望將費馬大定理引發的複雜數學思想轉化爲可編程的形式。

幾個世紀以來，爲了證明這個在Buzzard看來「毫無實際意義」的定理，人們開創了許多極具價值的新數學分支。

是的，在Buzzard看來，費馬大定理毫無意義，在現實世界中沒有任何應用，不過因爲這個「臭名昭著」的問題，幾個實際來人們產生了大量絕妙的新想法。

如今，將Wiles的100頁長的證明轉化爲計算機能夠理解的形式語言和規則，有望爲新一代數學家開啓計算機輔助證明的大門。

而這種轉換工具，也能夠爲編程人員提供幫助。

Littler表示，在這一領域，雄心勃勃的項目總是值得嘗試的，因爲我們都能從學到的經驗和編寫的程序庫中獲益。

交互式的定理證明雖然還是一個較新的領域，但Lean社區已經做了許多優秀的工作。

Kevin Buzzard：Lean的佈道者

1968年出生的Kevin Mark Buzzard，在算術幾何和Langlands程序方面有着深厚的專業造詣。

他目前是倫敦帝國學院的純數學教授，也是AI工具Lean的「佈道者」。

在皇家文法學校讀書期間，Kevin Buzzard曾參加了國際數學奧林匹克競賽，並在1986年贏得銅牌，1987年以滿分拿下金牌。

此後，他在劍橋大學的三一學院完成了數學本科學習，並於1990年獲得Senior Wrangler頭銜，於1991年獲得C.A.S.M.學位。

在Richard Taylor的指導下，他的博士論文「The levels of modular representations」於1995年完成，探討了數學中的一個複雜領域。

1998年，他開始在倫敦帝國學院擔任講師，2002年晉升爲高級講師，2004年被任命爲教授。

他還曾在哈佛大學（2002年10月至12月）和其他幾所著名機構進行訪問研究。

因其在數論領域的突出貢獻，他在2002年獲得了懷特黑德獎，2008年獲得了Senior Berwick獎。

2017年，Buzzard發起了一個關於Lean定理證明器的項目和博客，致力於推動在數學研究中使用計算機輔助證明工具。

他還指導了音樂家Dan Snaith（藝名Caribou）完成了關於超收斂Siegel模符號研究的數學博士論文，Snaith因此從倫敦帝國學院獲得了博士學位。

2023年10月，Kevin Buzzard在社交媒體上稱，自己獲得了研究經費，開始用Lean去證明費馬大定理。

Buzzard表示，「十年前，這需要花費無限多的時間」。爲了完成這個項目，他將把自己的教學任務擱置五年。

擱置自己的任務，值得嗎？

在他的同行、英國諾丁漢大學Chris Williams看來，這種項目可能會產生意想不到的好處，和深遠的影響。

「我認爲他不太可能在未來五年內正式形式化整個證明，否則就太驚人了。但是，現在的數論和算術幾何中，許多工具都無處不在，因此我預計，未來任何實質性的進展都將非常有用。」

對數學研究意義重大

這個項目還揭示了一個更深層次的價值。

隨着計算工具的不斷進步，數學的不同分支之間，甚至不同學科之間的界限，正變得越來越模糊，這就導致一些幾乎無法驗證的證明出現了。

比如，京都大學的日本數學家Mochizuki Shinichi編寫了一份長達500頁的證明，因爲太過複雜，花費了數年時間才發表出來，部分原因就是，人們不知道該如何處理它。

從此，我們可能會發現，數學的邊界變得越來越模糊。

這不是指真實性或邏輯上的模糊，而是指一個證明中可以融合的不同思想的範圍。

Lean可以讓數學家們的思想轉化爲代碼，這就讓同行更易於理解。看着前人記錄的先例，未來的數學家們可以在此基礎上繼續推進自己的研究。

Buzzard表示，用Lean進行數學寫作的特點就是，你可以留下精確陳述但未經證明的結果，而其他人就可以在之後解決它們。

Lean本身就促成了這樣一種工作流。

換言之，費馬大定理正準備以「衆包」的方式來解決——特別是如果編碼工作超出了Buzzard剩餘的工作年限。

完成一個數學證明需要整個社區的努力。

也許，在將來，我們能擁有一個類似Genius.com的平臺，用於分享和解讀數學證明。

參考資料：

https://www.popularmechanics.com/science/math/a60280173/machines-are-on-the-verge-of-tackling-fermats-last-theorema-proof-that-once-defied-them/

https://www.newscientist.com/article/2422601-mathematicians-plan-computer-proof-of-fermats-last-theorem/#Echobox=1710896989