一個有關數學形式化的有趣故事。

原標題：讓AI理解費馬大定理的證明，兩個月過去了，進展如何？
文章來源：機器之心
內容字數：7468字

費馬大定理證明的計算機形式化驗證：一個充滿挑戰與驚喜的故事

本文總結了倫敦帝國學院Kevin Buzzard教授及其團隊嘗試用計算機驗證費馬大定理證明的進展，以及過程中遇到的挑戰和意外收獲。

1. 項目目標與現狀

   Buzzard教授團隊的目標是教計算機理解費馬大定理（FLT）的現代證明，而非懷爾斯最初的證明。他們使用Lean證明器及其數學軟件庫mathlib進行形式化驗證。目前，團隊已完成部分抽象代數結果的證明，但仍未完成對關鍵概念“R”和“T”的完整定義。

2. 形式化驗證的意義

   該項目旨在探索AI是否能革新數學研究，并檢驗Lean證明器在現代數論研究中的作用。通過形式化驗證，計算機可以更好地理解現代數學定義，從而輔助人類突破數論難題。

3. 晶體上同調與除冪理論

   團隊在形式化過程中遇到了一個意想不到的挑戰：現代FLT證明中使用的晶體上同調理論，其基礎——除冪理論，在標準文獻中存在一個關鍵引理的錯誤。這個錯誤并非證明主要結論錯誤，但阻礙了形式化過程。

4. 發現錯誤與修正

   團隊成員Antoine Chambert-Loir發現了文獻中除冪理論的錯誤。這個錯誤并非微不足道，它影響了整個晶體上同調理論，甚至波及到Scholze等數學家的相關工作。然而，經過進一步研究，他們找到了Berthelot-Ogus著作附錄中另一個正確的證明，解決了這個問題。

5. 挑戰與反思

   這個故事揭示了現代數學文獻中存在的文檔化問題，許多被認為是“專家已知”的內容并未得到充分記錄。該項目強調了形式化數學的重要性，它能顯著降低錯誤的可能性。同時，它也說明了即使是重要的數學結論，其證明細節也可能存在疏漏，需要不斷完善。

6. 圓滿結局與未來展望

   最終，團隊成員Maria Ines解決了除冪理論的形式化問題，項目得以繼續推進。這個故事提醒人們重視數學的精確記錄，并為未來計算機輔助數學研究提供了寶貴經驗。

總而言之，Buzzard教授團隊的嘗試不僅在費馬大定理證明的形式化驗證方面取得了進展，更重要的是，它凸顯了形式化數學在提高數學精確性和推動數學發展中的重要作用，以及現代數學文獻中需要進一步改進的地方。

聯系作者

文章來源：機器之心
作者微信：
作者簡介：專業的人工智能媒體和產業服務平臺