资金费率
资金费率热力图
多空比
大户多空比
币安/欧易/火币大户多空比
Bitfinex杠杆多空比
账号安全
资讯收藏
自选币种
Anthropic宣布：Claude AI撰写史上最长数学证明，形式化验证费马大定理
Anthropic宣布，其人工智能模型Claude刚刚撰写了有史以来最长的数学证明，并以此形式化地证明了困扰数学家长达358年的“费马大定理”。整个验证过程仅耗时11天，且绝大部分由AI独立完成。Claude生成了1300万行代码，使得计算机能够逐行检查逻辑，而不再仅仅依赖数学家的口头陈述。
费马大定理指出：不可能存在三个正整数a、b和c，使得a的n次方加上b的n次方等于c的n次方，其中指数n大于2。1637年，皮埃尔·德·费马在一本数学书的页边空白处写下了这一论断，并声称自己发现了一个“真正奇妙的证明”，但页边的空间太小，无法容纳该证明的细节。随后，费马去世，接下来的358年里，无数数学家试图重构他脑海中可能存在的思路。
证明与验证：两项截然不同的工作
数学证明是一连串的逻辑步骤，任何一环断裂，整个论证便会崩塌。在数百页密集论证中找出那一个断裂的环节，往往需要其他数学家耗费数年心血。所谓“形式化证明”，是指将论证转化为一种极其严谨、字面意思明确的编程语言，使计算机能够在不介入主观判断的情况下，独立验证每一步骤的正确性。
长期以来，数学家在这一领域的自我监管并不完善。例如，1908年设立的一项德国奖项（按今日币值约合100万至200万美元），旨在奖励首个有效证明该定理的人，但在其第一年便收到了621份错误的投稿。
真正的证明直到1995年才出现，来自英国数学家安德鲁·怀尔斯（Andrew Wiles）。然而，这一成果伴随着戏剧性的转折。1993年6月，怀尔斯在三场讲座中公布了他的解法，但随后一位审稿人发现了其中的漏洞。他与前学生理查德·泰勒（Richard Taylor）合作，花了近一年时间修补漏洞，最终于1995年5月发表了一份经过修正的129页证明。该证明依赖于费马生前尚不存在的数学理论，这也是如今多数数学家怀疑费马所谓的“奇妙证明”实际上并不成立的主要原因。
Claude是如何做到的？
伦敦帝国理工学院数学家凯文·巴扎德（Kevin Buzzard）于2024年启动了一项项目，旨在完成Claude刚刚做的事：将怀尔斯的证明转化为Lean语言（一种可供计算机检查的形式化语言）。这是一项需要大量志愿者数学家参与的工作——该项目自身的提纲长达86页，且资金已锁定至2029年。而Claude仅用11天就完成了全部工作。
Anthropic在更深入的博客文章中解释道，哥伦比亚大学构建AI形式化工具的天一彭（Tianyi Peng）决定测试Claude在自主情况下的能力上限。数十个Claude代理并行工作，编写定义、证明小型结果，并将这些结果整合成更大的定理，人类干预极少，仅偶尔提示“优先处理下一个定理”。
起初进展并不顺利。早期，代理们经常迷失在已证明的内容中，导致协作中断。这些试错过程占最终证明代码的约7%。解决问题的关键是一款名为Prove2Me的工具，同样由Peng的团队开发。该工具为每个代理提供统一的实时待办事项列表，列出仍需完成的小型证明，从而避免重复工作或偏离方向。此外，它还优化了文件结构以加快Lean的检查速度，并为每个结果保留英文注释，以便代理们可以复用彼此的工作，而非重新发明轮子。
项目完成后，Claude证明了超过30,000个支撑定理，消耗了数十亿个Token。该任务运行在一个研究版模型上，Anthropic表示其性能大致相当于后来向公众发布的Claude 5.1版本。最终生成的证明长达1300万行，是数学家目前用于此类工作的共享库Mathlib规模的五倍以上。一部典型小说约为8万字，而Claude的证明相当于160部纯粹逻辑论证的小说。
这究竟有何意义？
巴扎德审查了Claude的证明并给予认可，称其“除了数学公理外，未作任何其他假设”便证明了该定理。但这并不意味着Claude发现了全新的数学知识——Anthropic今年早些时候在密码学研究中也曾提出类似主张。怀尔斯早在三十年前就已证明了费马大定理，Claude只是为其构建了一份机器可检查的“收据”。
这一点至关重要，因为数学家正日益被未经验证的证明所淹没，包括由AI撰写的证明，其增长速度远超人类手工核查的能力。此外，这类证明具有确定性，不易受人为错误影响，这在数学领域极为重要。
这并非新问题。开普勒猜想（Kepler conjecture）的计算机辅助证明耗时四年，评审委员会当时仅能承诺“99%确定”；格里戈里·佩雷尔曼（Grigori Perelman）对庞加莱猜想（Poincaré conjecture）的证明也经历了漫长的消化期。如果你不愿轻信Anthropic的说法，大可不必。这份完整的1300万行证明现存放于GitHub上，任何有足够闲暇时间的数学家均可逐行拆解查验。
