形式化费马最后定理
中文译文
最近，哥伦比亚大学人类学研究员Tianyi Peng （其团队构建了人工智能正式化的工具）开始测试Claude是否可以在FLT的正式化方面取得进展。结果比他预想的要更进一步。在11天内，大部分时间都在工作……
费马最后定理就是一个很好的例子。费马在书的空白处写下了这个定理的陈述，并附上一个诱人的注释：
多年来，几代数学家一直在寻找FLT的证据，无论是奇妙的还是其他的。1908年，宣布为任何能够提供正确证明的人颁发10万德国金马克（相当于今天的100-200万美元）的奖金， 6...
怀尔斯于1995年5月发表了FLT的第一个正确证明；它依赖的现代数学技术远远超出了费马在1637年所知道的。由于经过几个世纪的尝试还没有找到基本的证据，数学……
检查证明是否正确的一种方法是让计算机执行此操作。像精益这样的证明助手通过算法验证了证明的逻辑，毫无疑问地证明了它的正确性。对于人类来说，困难的部分是重写证据，以便精益可以理解……
Claude的证明遵循了Darmon、Diamond和Taylor对Wiles的证明的简化版本。人类的数学输入仅限于天一偶尔的高级指令： “雅可比作为一个方案听起来是高优先级的” ， “推动[该] Mazur [定理...
借助Prove2Me和基于Claude Code的多智能体线束，一组智能体在不到两周的时间内完成了验证，从大致与Claude Fable 5.1相当的通用内部研究模型中消耗了大约60亿个输出令牌。
我们能够生成这个证明的速度表明，现在可以形式化大量的数学，这既可以捕捉数学证明的共同体中的错误，也可以减轻裁判新作品的负担。经过修订...
形式化也是人类如何对人工智能生成的数学结果充满信心的一个主要因素。随着人工智能和人工智能辅助数学家产生比以往更多的（声称的）证明，人工智能辅助形式化承担了人类反馈的部分负担……
写作Lean似乎也有助于Claude证明新颖的结果。我们最近的许多克劳德撰写的结果已经与他们的证明同时正式化，克劳德似乎使用这些部分证明来独立检查其假设，就像它所写的那样……
正式化FLT是一个代币密集型项目，但它也是有史以来最大的精益证明。人类学研究人员使用三个个人Claude Max计划进行了一项小型实验，将Hardy-Littlewood Circle方法的应用正式化。Collabora...
为此， Anthropic和其他实验室最近扩大了对外部研究人员的支持，包括从事纯数学和形式化的数学家，提供免费和折扣订阅和研究学分。我们还提供专门的Gran...
随着人工智能迅速改变数学研究的样子，人类学和其他地方的数学家都在努力研究这对他们的工作意味着什么。然而，正规化是一个我们对人工智能的角色有着明确好感的地方。作为正规化……
我们的证明改编自Kevin Buzzard领导的伦敦帝国理工学院FLT项目和flt-regular项目。Lean和Mathlib都是他们自己的爱好，并收到了数百名数学家的贡献，其中许多人与Lea合作...
完整的证明可在GitHub上获得，以及证明的书面演练。
在这篇文章中，我们分享了两个结果，展示了Claude如何帮助生命科学家加快研究步伐。