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

AIGC動態歡迎閱讀

原標題：AI攻克費馬大定理？數學家放棄5年職業生涯，將100頁證明變代碼
關鍵字：定理,數學,解讀,數學家,項目
文章來源：新智元
內容字數：7550字

內容摘要：

新智元報道編輯：Aeneas 好困
【新智元導讀】困擾全世界幾個世紀的「臭名昭著」謎題——費馬大定理，或將被AI攻克？一位英國數學家宣布，即將啟動用Lean重現費馬大定理證明過程的項目，將100頁證明變成代碼。從此，世界頂尖數學難題的證明將成為「眾包」項目，你我都可以進去添幾筆。費馬大定理，即將被AI攻克？
而且整件事最意味深長的地方在于，AI即將解決的費馬大定理，正是為了證明AI無用。
曾經，數學屬于純粹的人類智力王國；如今，這片疆土正被先進的算法所破譯，所踐踏。
費馬大定理，是一個「臭名昭著」的謎題，在幾個世紀以來，一直困擾著數學家們。
它在1993年被證明，而現在，數學家們有一個偉大計劃：用計算機把證明過程重現。
他們希望在這個版本的證明中，如果有任何邏輯上的錯誤，都可由計算機檢查出來。
項目地址：https://github.com/riccardobrasca/flt3
3月底，數學家Pietro Monticone激動地表示，自己和同事幾乎在leanprover中完成了指數3的費馬大定理的形式化。
他們會盡快把形式化過程移植到Mathlib中，以便在FLT項目中使用。
證

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

聯系作者

文章來源：新智元
作者微信：AI_era
作者簡介：智能+中國主平臺，致力于推動中國從互聯網+邁向智能+新紀元。重點關注人工智能、機器人等前沿領域發展，關注人機融合、人工智能和機器人對人類社會與文明進化的影響，領航中國新智能時代。