AI 攻克费马大定理？数学家放弃 5 年职业生涯，将 100 页证明变代码
困擾全世界幾個世紀的「臭名昭著」謎題 —— 費馬大定理，或將被 AI 攻克？一位英國數學家宣布，即將啟動用 Lean 重現費馬大定理證明過程的項目，將 100 頁證明變成代碼。從此，世界頂尖數學難題的證明將成為「眾包」項目，你我都可以進去添幾筆。
費馬大定理，即將被 AI 攻克？而且整件事最意味深長的地方在于，AI 即將解決的費馬大定理，正是為了證明 AI 無用。
曾經，數學屬于純粹的人類智力王國；如今，這片疆土正被先進的算法所破譯，所踐踏。
費馬大定理，是一個「臭名昭著」的謎題，在幾個世紀以來，一直困擾著數學家們。
它在 1993 年被證明，而現在，數學家們有一個偉大計劃：用計算機把證明過程重現。
他們希望在這個版本的證明中，如果有任何邏輯上的錯誤，都可由計算機檢查出來。
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 經典入門游戲」。
她會用「自然數博弈」，幫學生熟悉數學歸納法的思想，通過「集合論博弈」，讓他們習慣于對集合進行推理。
在這個過程中，學生們對「嚴格遵循邏輯規則編寫證明」，和「用通俗語言解釋事物真理」之間的理解差距，就會逐漸彌合。
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
廣告聲明：文內含有的對外跳轉鏈接（包括不限于超鏈接、二維碼、口令等形式），用于傳遞更多信息，節省甄選時間，結果僅供參考，所有文章均包含本聲明。
總結
以上是生活随笔為你收集整理的AI 攻克费马大定理？数学家放弃 5 年职业生涯，将 100 页证明变代码的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： 宁德时代推出天恒 20 尺集装箱式储能系
- 下一篇： 破解 36 年前魔咒！Meta 推出反向