形式化费马大定理

我们正在分享费马大定理的第一个完整的计算机检查证明。 Claude 基本上自主工作了 11 天，用精益编程语言编写了证明。下面，我们描述了形式化是如何完成的，并分享了一些关于这项工作对研究数学意味着什么的想法。 1637 年左右，皮埃尔·德·费马 (Pierre de Fermat) 在他的《丢番图算术》副本的页边空白处记下了一个断言，该断言后来成为有史以来最著名的数学猜想之一：对于任何 n > 2，没有正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。费马大定理 (FLT)，正如该猜想所知道的那样，证明起来极其困难。第一份证明由安德鲁·怀尔斯 (Andrew Wiles) 爵士于 1995 年提供，长达 129 页，需要数月的艰苦工作才能验证。十年后，荷兰计算机科学家 Jan Bergstra 提出“形式化”怀尔斯的证明：将数学推理转换为计算机可以自动检查的形式。从那时起，数学家们一直在开发编码如此复杂的证明所需的方法，包括伦敦帝国理工学院的 Kevin Buzzard 于 2024 年启动的一项多年社区努力，以使用精益证明助手完成形式化。最近，哥伦比亚大学人类学研究员 Tianyi Peng 的团队开发了人工智能形式化工具，他开始测试 Claude 能否在形式化 FLT 方面取得进展。 1 结果超出了他的预期。在 11 天的时间里，克劳德基本上是自主工作，制作了第一个端到端、计算机检查的 FLT 证明。一路走来，它编写了 1300 万行 Lean 代码，并证明了 29,500 个中间定理。我们与 Kevin Buzzard 分享了最终的证明，他说：这项非凡的自动形式化成就（人类学研究人员称只花了 11 天）就证明了费马大定理，除了数学公理之外没有任何假设。一路走来，我们看到了代数、调和分析、几何和数论的自动形式化，并且我们了解到人工智能自动形式化制品现在已经足够强大，可以在其上构建；证明是多层次的。自动形式化像 FLT 这样复杂的证明是迈向所有数学都可以轻松检查的未来的重要一步。随着人工智能产生越来越多的证据，轻松地将工作形式化的能力可以减轻评估新结果的负担（这个过程可能需要数年时间）。我们希望相信数学赖以建立的知识体系会变得更容易，而不是更困难。验证数学证明的挑战与最近人工智能驱动的黎曼假设研究不同，该研究产生了新颖的数学，这里的新颖之处在于验证——检查数学证明，就像用计算器检查数学计算一样。证明数学定理需要组装复杂的逻辑链，如果单个链接被破坏，它后面的所有内容都可能被证明是错误的。深入理解一个新颖的结果并对其正确性充满信心可能需要数月甚至数年的工作。费马大定理就是一个说明性的例子。 2 费马在一本书的页边空白处写下了这个定理的陈述，并附上了一条诱人的注释：我发现了一个真正奇妙的证明，这个页边空白太窄了，无法容纳。 350 多年来，一代又一代的数学家一直在寻找 FLT 的证明，无论是奇妙的还是其他的。 1908 年，宣布奖励 10 万德国金马克（相当于今天的 1-200 万美元），奖励任何能够提出正确证明的人，仅第一年就有 621 次错误尝试。 1993 年 6 月，怀尔斯在为期三天的系列讲座中提出了他认为是 FLT 的第一个正确证明。经过几位数学家的密集验证工作两个月后，一位审稿人向怀尔斯提出了一个暴露了关键差距的问题。怀尔斯花了一年的时间试图解决这个问题，首先是独自一人，然后是与他以前的学生理查德泰勒一起。当他终于意识到他之前放弃的方法可以修复证明时，他正处于放弃该项目的边缘。 Wiles于1995年5月发表了FLT的第一个正确证明；它所依赖的现代数学技术远远超出了 1637 年费马所知道的技术。由于经过几个世纪的尝试仍未找到基本证明，数学界现在认为费马自己最初的“奇妙证明”是不正确的。形式化费马大定理 检查证明正确性的一种方法是让计算机来做这件事。像 Lean 这样的证明助手通过算法验证证明的逻辑，毫无疑问地证明其正确性。对于人类来说，困难的部分是重写证明，以便精益能够理解它。虽然为人类读者编写的证明会跳过许多明显的步骤，但精益需要查看每一个步骤，无论多么微不足道。人类证明也建立在几个世纪以来已发表的工作的基础上，而形式化则从微小的裂缝开始