新智元報(bào)道
編輯：Aeneas 好困
【新智元導(dǎo)讀】困擾全世界幾個(gè)世紀(jì)的「臭名昭著」謎題費(fèi)馬大定理，或?qū)⒈籄I攻克？一位英國(guó)數(shù)學(xué)家宣布，即將啟動(dòng)用Lean重現(xiàn)費(fèi)馬大定理證明過程的項(xiàng)目，將100頁證明變成代碼。從此，世界頂尖數(shù)學(xué)難題的證明將成為「眾包」項(xiàng)目，你我都可以進(jìn)去添幾筆。
費(fèi)馬大定理，即將被AI攻克？
而且整件事最意味深長(zhǎng)的地方在于，AI即將解決的費(fèi)馬大定理，正是為了證明AI無用。
曾經(jīng)，數(shù)學(xué)屬于純粹的人類智力王國(guó)；如今，這片疆土正被先進(jìn)的算法所破譯，所踐踏。
費(fèi)馬大定理，是一個(gè)「臭名昭著」的謎題，在幾個(gè)世紀(jì)以來，一直困擾著數(shù)學(xué)家們。
它在1993年被證明，而現(xiàn)在，數(shù)學(xué)家們有一個(gè)偉大計(jì)劃：用計(jì)算機(jī)把證明過程重現(xiàn)。
他們希望在這個(gè)版本的證明中，如果有任何邏輯上的錯(cuò)誤，都可由計(jì)算機(jī)檢查出來。
項(xiàng)目地址：https://github.com/riccardobrasca/flt3
3月底，數(shù)學(xué)家Pietro Monticone激動(dòng)地表示，自己和同事幾乎在leanprover中完成了指數(shù)3的費(fèi)馬大定理的形式化。
他們會(huì)盡快把形式化過程移植到Mathlib中，以便在FLT項(xiàng)目中使用。
證明過程大致遵循Wiles的證明，但會(huì)略有改動(dòng)。
用Lean把費(fèi)馬大定理變成代碼
當(dāng)四月到來時(shí)，數(shù)學(xué)家兼程序員Kevin Buzzard將發(fā)布這個(gè)計(jì)劃：通過計(jì)算機(jī)代碼，完成費(fèi)馬大定理的證明。
項(xiàng)目在4月上線后，公開的藍(lán)圖就會(huì)出現(xiàn)在網(wǎng)上，屆時(shí)，Lean社區(qū)的任何人，都可以為形式化證明做出自己的貢獻(xiàn)。
把一個(gè)開創(chuàng)性的100頁數(shù)學(xué)證明，變成計(jì)算機(jī)代碼，這個(gè)過程容易實(shí)現(xiàn)嗎？
這當(dāng)然就要?dú)w功于被陶哲軒大加贊賞、沉迷使用的證明工具Lean，它可以讓用戶把散文式的證明轉(zhuǎn)化為用于測(cè)試的規(guī)則和邏輯。
但無論如何，這項(xiàng)工程都不簡(jiǎn)單，預(yù)計(jì)將歷時(shí)多年，而Kevin Buzzard頁獲得了項(xiàng)目的資金支持。
大家都明白，這個(gè)項(xiàng)目，很可能是迄今為止最復(fù)雜的計(jì)算機(jī)化方式證明之一。
費(fèi)馬大定理
費(fèi)馬大定理，堪稱是史上最精彩的一個(gè)數(shù)學(xué)謎題。
而證明費(fèi)馬大定理的過程，直接就是一部數(shù)學(xué)史。
我們耳熟能詳?shù)馁M(fèi)馬大定理，由17世紀(jì)的法國(guó)數(shù)學(xué)家皮埃爾德費(fèi)馬提出。遺憾的是，他未能在有生之年找到證明。
于是，這項(xiàng)起源于三百多年前的難題，直接挑戰(zhàn)了人類整整3個(gè)世紀(jì)，多次震驚全世界，耗盡人類眾多最杰出大腦的精力，也讓千千萬萬業(yè)余者癡迷。
這個(gè)定理聲稱，不存在三個(gè)正整數(shù)a、b、c能滿足方程 (a^n + b^n = c^n)，其中n是任何大于2的整數(shù)。
這個(gè)證明的難點(diǎn)就在于，數(shù)學(xué)家很難找出一個(gè)否定案例：我們?cè)趺茨鼙ＷC一定不存在這樣一個(gè)無窮大的整數(shù)n，能滿足這個(gè)方程式呢？
幸好，對(duì)于今天的數(shù)學(xué)家來說，將無窮大的概念轉(zhuǎn)換成邏輯，并不是什么新鮮事了。
在較為簡(jiǎn)單的證明中，我們可以依靠歸納法
一旦某個(gè)邏輯對(duì)某個(gè)數(shù)字成立（比如8），那么它對(duì)于之后的每一個(gè)數(shù)（比如9、10、11等）都同樣成立，直到無限大。
然而，費(fèi)馬大定理卻是數(shù)學(xué)界百年來的一塊絆腳石。
直到1993年，英國(guó)數(shù)學(xué)家Andrew Wiles用一份長(zhǎng)達(dá)100頁的書面證明，解開了這一謎團(tuán)。
計(jì)算機(jī)為什么無法證明費(fèi)馬大定理？
業(yè)界認(rèn)為原因有三：
1. 計(jì)算機(jī)無法推導(dǎo)出無窮種
2. 計(jì)算機(jī)無法證明邏輯正確
3. 計(jì)算機(jī)可能會(huì)出現(xiàn)轉(zhuǎn)瞬即逝的失誤
幸好有Lean輔助證明
一份100頁的數(shù)學(xué)證明，無論是對(duì)于普通的數(shù)學(xué)系學(xué)生，還是數(shù)學(xué)家，都不是那么好駕馭的。
好在，我們可以不再依賴傳統(tǒng)的證明方法，可以求助于Lean這樣的工具。
它是一款基于C++開發(fā)的編程工具，專為編寫和驗(yàn)證歸納法證明而設(shè)計(jì)。
如今許多所謂的「人工智能」，不過是巧妙地排列模仿人類語言的文字。但Lean這類計(jì)算機(jī)輔助的證明，更深入地融合了人類的思維方式，和計(jì)算機(jī)輔助加強(qiáng)的能力。
Lean編程工具，進(jìn)入本科課堂
在倫敦帝國(guó)理工學(xué)院教數(shù)學(xué)的Kevin Buzzard，花費(fèi)了數(shù)年時(shí)間，利用Lean為學(xué)院的整個(gè)本科數(shù)學(xué)課程開發(fā)了支持工具。
通過這些工具，學(xué)生們可以將課堂上討論的內(nèi)容分解成邏輯和數(shù)學(xué)運(yùn)算的步驟。
這就仿佛是一個(gè)數(shù)學(xué)證明上的羅塞塔石碑。
同為數(shù)學(xué)教師的Clarissa Littler，就非常贊同Kevin Buzzard的理念。
她在波特蘭社區(qū)學(xué)院教授離散數(shù)學(xué)。過去兩個(gè)學(xué)期里，她都在離散數(shù)學(xué)課上用Kevin Buzzard開發(fā)的「Lean經(jīng)典入門游戲」。
她會(huì)用「自然數(shù)博弈」，幫學(xué)生熟悉數(shù)學(xué)歸納法的思想，通過「集合論博弈」，讓他們習(xí)慣于對(duì)集合進(jìn)行推理。
在這個(gè)過程中，學(xué)生們對(duì)「嚴(yán)格遵循邏輯規(guī)則編寫證明」，和「用通俗語言解釋事物真理」之間的理解差距，就會(huì)逐漸彌合。
Littler強(qiáng)調(diào)，課程的一大重點(diǎn)，就是讓數(shù)學(xué)基礎(chǔ)不太牢固的學(xué)生，更自如地用數(shù)學(xué)家的方式思考，同時(shí)更好地理解證明、證據(jù)和展示真理的方法。
這種從形式邏輯到規(guī)則列表，再到用散文表達(dá)的轉(zhuǎn)變，是將項(xiàng)目分解成互相協(xié)作的代碼片段的關(guān)鍵所在。
而這一點(diǎn)，在編程和純數(shù)學(xué)的交叉領(lǐng)域尤為重要，也正是Lean這樣的工具能大放異彩的地方。
Buzzard表示，他希望將費(fèi)馬大定理引發(fā)的復(fù)雜數(shù)學(xué)思想轉(zhuǎn)化為可編程的形式。
幾個(gè)世紀(jì)以來，為了證明這個(gè)在Buzzard看來「毫無實(shí)際意義」的定理，人們開創(chuàng)了許多極具價(jià)值的新數(shù)學(xué)分支。
是的，在Buzzard看來，費(fèi)馬大定理毫無意義，在現(xiàn)實(shí)世界中沒有任何應(yīng)用，不過因?yàn)檫@個(gè)「臭名昭著」的問題，幾個(gè)實(shí)際來人們產(chǎn)生了大量絕妙的新想法。
如今，將Wiles的100頁長(zhǎng)的證明轉(zhuǎn)化為計(jì)算機(jī)能夠理解的形式語言和規(guī)則，有望為新一代數(shù)學(xué)家開啟計(jì)算機(jī)輔助證明的大門。
而這種轉(zhuǎn)換工具，也能夠?yàn)榫幊倘藛T提供幫助。
Littler表示，在這一領(lǐng)域，雄心勃勃的項(xiàng)目總是值得嘗試的，因?yàn)槲覀兌寄軓膶W(xué)到的經(jīng)驗(yàn)和編寫的程序庫中獲益。
交互式的定理證明雖然還是一個(gè)較新的領(lǐng)域，但Lean社區(qū)已經(jīng)做了許多優(yōu)秀的工作。
Kevin Buzzard：Lean的布道者
1968年出生的Kevin Mark Buzzard，在算術(shù)幾何和Langlands程序方面有著深厚的專業(yè)造詣。
他目前是倫敦帝國(guó)學(xué)院的純數(shù)學(xué)教授，也是AI工具Lean的「布道者」。
在皇家文法學(xué)校讀書期間，Kevin Buzzard曾參加了國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽，并在1986年贏得銅牌，1987年以滿分拿下金牌。
此后，他在劍橋大學(xué)的三一學(xué)院完成了數(shù)學(xué)本科學(xué)習(xí)，并于1990年獲得Senior Wrangler頭銜，于1991年獲得C.A.S.M.學(xué)位。
在Richard Taylor的指導(dǎo)下，他的博士論文「The levels of modular representations」于1995年完成，探討了數(shù)學(xué)中的一個(gè)復(fù)雜領(lǐng)域。
1998年，他開始在倫敦帝國(guó)學(xué)院擔(dān)任講師，2002年晉升為高級(jí)講師，2004年被任命為教授。
他還曾在哈佛大學(xué)（2002年10月至12月）和其他幾所著名機(jī)構(gòu)進(jìn)行訪問研究。
因其在數(shù)論領(lǐng)域的突出貢獻(xiàn)，他在2002年獲得了懷特黑德獎(jiǎng)，2008年獲得了Senior Berwick獎(jiǎng)。
2017年，Buzzard發(fā)起了一個(gè)關(guān)于Lean定理證明器的項(xiàng)目和博客，致力于推動(dòng)在數(shù)學(xué)研究中使用計(jì)算機(jī)輔助證明工具。
他還指導(dǎo)了音樂家Dan Snaith（藝名Caribou）完成了關(guān)于超收斂Siegel模符號(hào)研究的數(shù)學(xué)博士論文，Snaith因此從倫敦帝國(guó)學(xué)院獲得了博士學(xué)位。
2023年10月，Kevin Buzzard在社交媒體上稱，自己獲得了研究經(jīng)費(fèi)，開始用Lean去證明費(fèi)馬大定理。
Buzzard表示，「十年前，這需要花費(fèi)無限多的時(shí)間」。為了完成這個(gè)項(xiàng)目，他將把自己的教學(xué)任務(wù)擱置五年。
擱置自己的任務(wù)，值得嗎？
在他的同行、英國(guó)諾丁漢大學(xué)Chris Williams看來，這種項(xiàng)目可能會(huì)產(chǎn)生意想不到的好處，和深遠(yuǎn)的影響。
「我認(rèn)為他不太可能在未來五年內(nèi)正式形式化整個(gè)證明，否則就太驚人了。但是，現(xiàn)在的數(shù)論和算術(shù)幾何中，許多工具都無處不在，因此我預(yù)計(jì)，未來任何實(shí)質(zhì)性的進(jìn)展都將非常有用�！�
對(duì)數(shù)學(xué)研究意義重大
這個(gè)項(xiàng)目還揭示了一個(gè)更深層次的價(jià)值。
隨著計(jì)算工具的不斷進(jìn)步，數(shù)學(xué)的不同分支之間，甚至不同學(xué)科之間的界限，正變得越來越模糊，這就導(dǎo)致一些幾乎無法驗(yàn)證的證明出現(xiàn)了。
比如，京都大學(xué)的日本數(shù)學(xué)家Mochizuki Shinichi編寫了一份長(zhǎng)達(dá)500頁的證明，因?yàn)樘^復(fù)雜，花費(fèi)了數(shù)年時(shí)間才發(fā)表出來，部分原因就是，人們不知道該如何處理它。
從此，我們可能會(huì)發(fā)現(xiàn)，數(shù)學(xué)的邊界變得越來越模糊。
這不是指真實(shí)性或邏輯上的模糊，而是指一個(gè)證明中可以融合的不同思想的范圍。
Lean可以讓數(shù)學(xué)家們的思想轉(zhuǎn)化為代碼，這就讓同行更易于理解�？粗叭擞涗浀南壤磥淼臄�(shù)學(xué)家們可以在此基礎(chǔ)上繼續(xù)推進(jìn)自己的研究。
Buzzard表示，用Lean進(jìn)行數(shù)學(xué)寫作的特點(diǎn)就是，你可以留下精確陳述但未經(jīng)證明的結(jié)果，而其他人就可以在之后解決它們。
Lean本身就促成了這樣一種工作流。
換言之，費(fèi)馬大定理正準(zhǔn)備以「眾包」的方式來解決特別是如果編碼工作超出了Buzzard剩余的工作年限。
完成一個(gè)數(shù)學(xué)證明需要整個(gè)社區(qū)的努力。
也許，在將來，我們能擁有一個(gè)類似Genius.com的平臺(tái)，用于分享和解讀數(shù)學(xué)證明。
參考資料：
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
