AI去啃费马大定理：帝国理工用机器逐行核对世纪难题，能啃的只有边角料

当所有人都在用AI写PPT、烧钱抢芯片时，有一群数学家在伦敦干了件冷门事：让AI去核对费马大定理的证明。

三个关键信息

7月6日到10日，帝国理工学院办了一场闭门工作坊，主题是把费马大定理的证明翻译成机器能验证的代码。 项目由数学家Kevin Buzzard领衔，用的是Lean定理证明器，目标是把整套证明搬进数学公共库Mathlib。这个项目拿了英国EPSRC的经费，一直资助到2029年——光是把一个已经被证明的定理翻译给机器看，就要干上好几年。

给工作坊掏钱的是一家叫Logos Research的科技公司，他们想试一件事：让AI来干这个翻译活。 术语叫「自动形式化」（autoformalization）——把人类写的数学证明，自动改写成Lean能一行行核对、挑不出错的形式化代码。随着AI越来越强，他们想看看到底哪些部分机器能接手。

答案很诚实：AI只能啃边角料。 团队的判断是，那些定义繁多、概念抽象的硬核部分，AI大概率搞不定；而那些定义都已经在Mathlib里备好、人类文献又写得清清楚楚的部分，AI才可能派上用场。他们要形式化的还不是当年怀尔斯（Wiles）1994年那版原始证明，而是一个更现代的版本。

王斗视角

这条新闻没有几十亿美元的估值，也没有发布会，但它比大部分AI新闻都诚实。硅谷天天喊AI马上要取代程序员、取代科学家，可真把它拉到费马大定理面前——数学界公认最难啃的证明之一——它能干的只是搬运工的活：把定义已经摆好、人类已经写明白的段落，誊写成机器格式；稍微硬一点、需要真正想清楚的地方，还得数学家自己上。这就是当下AI最真实的水位：它是个不知疲倦、还算靠谱的抄写员，离「自己想出证明」差得远。一个已经被证明了三十年的定理，翻译给机器看都要花到2029年，你就知道那些说「AI明年就能做原创科研」的人，吹得有多离谱。真金白银的智能，不是看它PPT做得多花哨，是看它敢不敢站到费马这种题目面前——而它现在，只敢站在门口搬砖。

来源：Xena / Kevin Buzzard · Imperial College FLT · Science News