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在閱讀形式化證明時能檢查其中錯誤。