第412期：史上最长的数学程序

上周，Anthropic 公司使用 Claude AI，完成了一个史上最长的数学程序：程序化证明了费马大定理。17世纪，法国数学家费马提出一个著名猜想：大于2的整数，不可能满足下面的等式。后世的数学家发现，这个猜想难得超乎想象，根本无法证明。直到三百多年后的1995年，英国数学家安德鲁·怀尔斯才最终证明了费马大定理是正确的。安德鲁·怀尔斯的证明一共有129页，即使是专业的数学家也要花几个月才能读懂。

自从这个证明提出后，数学界一直致力于将它翻译成计算机语言，实现机器证明，从而可以自动化验证推理过程。这个从人工证明到机器证明的翻译项目，也是超难，工作量超大，迟迟没有完成。直到上周，一个研究团队宣布，Claude AI 用了11天终于完成了，将安德鲁·怀尔斯的证明翻译成了 Lean 语言的程序。Lean 语言是微软研究院 2013年提出的一种专门用于数学定理证明的编程语言。

研究人员本来只是想试一下 Claude AI 的数学研究能力，没想到它真的完成了这个超难的、无人完成的项目。在证明最终结果前，Claude 先证明了超过3万个辅助定理，用到了其中2万9千多个，消耗了数十亿的 Token，最终代码长达1300万行。这是有史以来最长的数学程序，不敢想象如果让人类的一个数学家团队来写要多久？所有代码现在就公布在 GitHub 上面。

这件事情的意义在于，现在有大量的数学证明，无法验证是否正确，即使是数学家也要花很多时间才能看懂。现在，事实证明，AI 可以用来验证这些证明是否正确。最后，这里有一篇安德鲁·怀尔斯专访，他讲述自己的人生故事，推荐给大家。采访者问他：“你为了证明费马大定理，苦苦探索了这么多年。这段旅程现在结束了，你想必会有点伤感吧？”安德鲁回答说，就像打完一场大战，感觉解脱了。

“确实有些伤感，但同时也有一种巨大的成就感，还感到终于自由了。我曾如此痴迷于这个问题，无时无刻不在思考它——早上醒来，晚上入睡——这种情况持续了八年。长时间思考一件事，确实很不容易。这段特殊的历程现在终于结束了，我的内心终于平静下来了。”