AI攻克費馬大定理？數(shù)學(xué)家放棄5年職業(yè)生涯，將100頁證明變代碼

AIGC動態(tài)歡迎閱讀

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

內(nèi)容摘要：

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

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

聯(lián)系作者

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