Claude用11天完成费马大定理首个计算机核验证明

Anthropic 9月7日宣布,Claude模型在基本自主运行约11天后,完成费马大定理首个端到端、经计算机检查的Lean形式化证明。整套证明基于Lean 4.33.1与Mathlib,6万多个模块全部通过内核检查,无未竟证明、无新增公理,并以Apache 2.0协议开源。数学家Kevin Buzzard评价称若FLT自动化证明可行,我们已朝自动形式化现代数学文献迈出一大步。OpenAI的GPT-6 Astra同期将孪生素数间隔上限降至186,AI数学能力密集突破引发范式转变。