第412期：史上最長的數學程序

上週，Anthropic 公司使用 Claude AI，完成了一個史上最長的數學程序：程序化證明了費馬大定理。17世紀，法國數學家費馬提出一個著名猜想：大於2的整數，不可能滿足下面的等式。後世的數學家發現，這個猜想難得超乎想象，根本無法證明。直到三百多年後的1995年，英國數學家安德魯·懷爾斯才最終證明了費馬大定理是正確的。安德魯·懷爾斯的證明一共有129頁，即使是專業的數學家也要花幾個月才能讀懂。

自從這個證明提出後，數學界一直致力於將它翻譯成計算機語言，實現機器證明，從而可以自動化驗證推理過程。這個從人工證明到機器證明的翻譯項目，也是超難，工作量超大，遲遲沒有完成。直到上週，一個研究團隊宣佈，Claude AI 用了11天終於完成了，將安德魯·懷爾斯的證明翻譯成了 Lean 語言的程序。Lean 語言是微軟研究院 2013年提出的一種專門用於數學定理證明的編程語言。

研究人員本來只是想試一下 Claude AI 的數學研究能力，沒想到它真的完成了這個超難的、無人完成的項目。在證明最終結果前，Claude 先證明了超過3萬個輔助定理，用到了其中2萬9千多個，消耗了數十億的 Token，最終代碼長達1300萬行。這是有史以來最長的數學程序，不敢想象如果讓人類的一個數學家團隊來寫要多久？所有代碼現在就公佈在 GitHub 上面。

這件事情的意義在於，現在有大量的數學證明，無法驗證是否正確，即使是數學家也要花很多時間才能看懂。現在，事實證明，AI 可以用來驗證這些證明是否正確。最後，這裏有一篇安德魯·懷爾斯專訪，他講述自己的人生故事，推薦給大家。採訪者問他：“你爲了證明費馬大定理，苦苦探索了這麼多年。這段旅程現在結束了，你想必會有點傷感吧？”安德魯回答說，就像打完一場大戰，感覺解脫了。

“確實有些傷感，但同時也有一種巨大的成就感，還感到終於自由了。我曾如此癡迷於這個問題，無時無刻不在思考它——早上醒來，晚上入睡——這種情況持續了八年。長時間思考一件事，確實很不容易。這段特殊的歷程現在終於結束了，我的內心終於平靜下來了。”

來源｜阮一峯科技愛好者週刊第 412 期，https://github.com/ruanyf/weekly/blob/master/docs/issue-412.md