[爆卦] AI在閱讀費馬大定理證明時發現小錯誤

[jackliao1990 (j)]

https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/

1637年費馬在《算術》拉丁文譯本的第11卷第8命題旁寫道："將一個立方數分成兩個立方
數之和，或一個四次冪分成兩個四次冪之和，或一般地將一個高於二次的冪分成兩個同次
方之和，這是不可能的。空白處太小，寫不下。"

這就是費馬大定理，直到1995年Andrew Wiles才透過建立模形式和橢圓曲線間的聯繫證明
它。而為了將費馬大定理的證明形式化(將人類數學邏輯轉成電腦邏輯)，倫敦帝國學院的
Kevin Buzzard用Lean及mathlib將費馬大定理證明形式化後再餵給AI。

兩個月後Buzzard在他部落格表示:目前大部分訓練都是在教AI"懷爾斯證明的「R=T」定理
中的抽象環R和T是什麼"，AI目前正在理解這些抽象環的定義。而當AI讀到"如何透過除冪
理論導出晶體上同調的關鍵結構"時，AI發現Roby引理中有缺陷!

為了挽救形式化證明，Buzzard在伊斯靈頓的咖啡店將此危機告訴時枝正，時枝正回到史
丹佛後跟Brian Conrad提及此事，Conrad翻查文獻後發現Berthelot-Ogus附錄中另一證明
方式，這才解決了缺陷。

此專案證實了形式化的重要，任何人類「這看起來沒問題」的表述都需具備形式化的邏輯
基礎，AI在閱讀形式化證明時能檢查其中錯誤。

--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 111.253.185.226 (臺灣)
※ 文章網址: https://www.ptt.cc/bbs/Gossiping/M.1735383043.A.DD7.html
推 zoeapezoo: 跟我
推 Calcifer: 跟我國中做題目ㄉ時候想到ㄉ雷同
推 toto3527: 看不懂啦 三小
推 s902131: 我五年前就發現了 現在才知道?
→ a27588679: 我以前發現還被老師罵說不可能有錯
推 AgentSkye56: 跟我想的一樣
推 milk7054: 可以把北檢起訴書丟給chatgpt評論嗎
→ Xenia1050: 我以前發現還被老師罵說不可能有錯
推 rainingkid: 我國中的時候和數學老師講他還不信
→ yc0304: 形式化證明跟當今講的AI完全是兩回事
推 reich3: 每一個中文字我都認識，但.....
推 xaxa0101: 我國中的數學老師跟我講我還不信
推 diyaworld: 上次我要寫這題的論文，老師叫我不要
→ diyaworld: 寫
→ Rexmax: 我早就發現
推 pokiman: 跟Ai討論物理才會惱火
→ johnson2726: 我早就發現了 老師還說是我想太多
推 gginin007: 供三小
推 tiramisu0225: 跟我想的一樣
推 a12841: 我也是這樣覺得
噓 inoce: 早就知道了 老師雞掰還規定只能用課堂上教
→ inoce: 的來解 不然一律算錯
推 js0431: 共三小 嗚嗚嗚
噓 iAsshole: 推文果然和我想的一樣。
推 azeroth: 咩嚕咩嚕咩
推 create8: 幹，還有幾集可逃？
推 mikiji: 跟我
→ mengze3084: 所以禮拜一要買哪一隻股票
推 RLH: 有問題的是轉述成給AI閱讀的形式吧
推 zxcvbnmnbvcx: 已知用火
推 abdiascat: 大家都進化成我看不懂的樣子了嗚嗚嗚
推 sufferlove: 所以就是對的東西，AI看不懂。