安索普公司表示，其克劳德人工智能刚刚写出了有史以来最长的数学证明，并利用它正式证明了费马最后定理，这是一个让数学家们困惑了358年的问题。

克劳德在11天内完成了这一任务，主要是凭借自己的能力，生成了1300万行代码，计算机可以逐行检查，而不是仅仅依赖数学家的说法。

费马最后定理表示，你不能取三个正整数，将每个数提升到大于2的幂，并让前两个数加起来等于第三个数。他在1637年写下这一主张在一本数学书的边缘，补充说他有一个“真正奇妙的证明”，但这个边缘实在太小，无法放下。

随后他去世了。数学家们在接下来的358年里试图重建他认为拥有的证据。

证明某事与检查它是两项不同的工作

数学证明是一个逻辑步骤的链条，如果一个环节断裂，整个证明就会崩溃。找到那个被埋藏在百页密集论证中的断链，可能需要其他数学家花费数年时间。

使证明正式化意味着将其翻译成一种极其字面化的语言，以便计算机可以独立验证每一步，而不涉及主观性。

数学家们对此的监管一直很糟糕。1908年颁发的德国奖项，今天相当于约100万到200万美元，奖励首个有效的该定理证明，在第一年就收到了621个错误的提交。

直到1995年，来自英国数学家安德鲁·怀尔斯的真正证明才出现，并且伴随了一次剧情反转。怀尔斯在1993年6月的三次讲座中宣布了他的解决方案，没过多久，一位审查员又发现了漏洞。

他与前学生理查德·泰勒花费了近一年时间修正，几乎放弃，最后在1995年5月发表了一份修正后的129页证明。这证明依赖于费马生前不存在的数学，这也是数学家们现在怀疑费马的“奇妙证明”是否实际上有效的重要原因。

伦敦帝国学院的数学家凯文·巴扎德于2024年启动了一个项目，正好做克劳德刚刚做的事情：将怀尔斯的证明翻译成计算机可以检查的Lean语言。这一工作需要一支志愿者数学家的团队——该项目的提纲长达86页，资金锁定至2029年。

克劳德在11天内完成了整个任务。

克劳德是如何做到的

安索普公司在更深入的帖子中解释，田毅彭与哥伦比亚大学的团队一起构建人工智能形式化工具，决定看看克劳德能独立完成多少任务。数十个克劳德代理并行工作，编写定义、证明小结果，并将这些结果组合成更大的结果，几乎没有人类输入，除了偶尔的提示，例如“下一个优先考虑这个定理”。

一开始并不顺利。早期，代理们不断失去对已证明内容的跟踪，并停止协作，而这些错误的开始仍然占据最终证明中约7%的行数。

解决此问题的工具是Prove2Me，也是彭的团队构建的，它为每个代理提供了相同的实时待办事项列表，指出哪些较小的证明仍需要完成，因此没有人重复劳动或迷失方向。它还组织文件，以便Lean可以更快地检查所有内容，并在每个结果上保留简明的英文笔记，以便代理们可以重复使用彼此的工作，而不是重新发明轮子。

完成时，克劳德证明了超过30,000个支持定理，并花费了数十亿个代币，运行在安索普公司所称的与克劳德Fable 5.1大致相当的研究模型上，后者是后来发布给公众的版本。最终的证明包含1300万行——是数学家们已用于此类工作的共享库Mathlib的五倍以上。

一本典型的小说约有80,000个单词。克劳德的证明相当于160本纯逻辑论证的小说。

这真的重要吗？

巴扎德——他的项目版仍然资助至2029年——审查了克劳德的证明，并给予了肯定，表示它证明了该定理“没有其他假设，除了数学公理。”

这并不等于克劳德发现了全新的数学，安索普今年早些时候在其密码学研究中也声称过这一点。怀尔斯三十年前已经证明了费马的定理——克劳德只是构建了一个可以计算机检查的收据。这一点很重要，因为数学家们越来越多地面临未验证的证明，包括人工智能编写的证明，速度更快于人类手动检查的能力。

此外，这些类型的证明是确定性的，不容易出现人为错误，这在数学中非常重要。

这并不是一个新问题。一项基于计算机的凯普勒猜想证明花了四年时间，评审小组仅能确认“99%确定”，而格里戈里·佩雷尔曼的庞加莱猜想证明也花费了大约同样长的时间才能完全被理解。

如果你不想仅仅依赖安索普公司的说法，你完全可以。完整的1300万行证明现在正在GitHub上，任何有足够空闲时间的数学家都可以逐行挑剔。

免责声明：本文章仅代表作者个人观点，不代表本平台的立场和观点。本文章仅供信息分享，不构成对任何人的任何投资建议。用户与作者之间的任何争议，与本平台无关。如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到support@aicoin.com，本平台相关工作人员将会进行核查。