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在阅读形式化证明时能检查其中错误。