【费马大定理的 AI 时刻：11 天跨越 350 年的数学鸿沟】Anthropic宣布Claude仅耗时11天便完成了费马大定理的Lean语言形式化证明，产出1300万行代码并验证了近3万个中间定理。这件事的本质不是AI发现了新数学，而是它完成了一次史诗级的“代码移植”——将人类已知的复杂证明翻译成计算机可验证的逻辑语言。这一进展最震撼之处在于效率的降维打击：人类团队原本预算100万英镑、计划耗时5年的项目，被AI以约30万美元的Token成本在两周内“暴力拆解”。虽然1300万行代码被不少圈内人吐槽为缺乏抽象美感的“逻辑屎山”，甚至有人担心AI可能利用了Lean内核的潜在漏洞来“作弊”，但它确实证明了Agent协作能够处理极长程的逻辑链条。对于研究者而言，这并不意味着数学家的失业，而是审稿压力的解放。未来数学论文可能必须附带形式化代码，由机器负责逻辑闭环，人类负责直觉与创新。我们正站在一个奇点：当证明的正确性不再依赖于少数天才的肉眼复核，科学发现的迭代速度将彻底脱离生物大脑的物理限制。