跨越三百年的数学难题迎来机器验证里程碑
费马大定理是数论领域最富传奇色彩的未解难题之一。1637年，法国数学家皮埃尔·费马在丢番图《算术》一书的页边空白处写下了一条断言：对于任何大于2的正整数n，不存在满足aⁿ + bⁿ = cⁿ的正整数组合a、b、c。费马同时附上了一句令人遐想的注记——「我发现了一个奇妙的证明，但这里的空白太窄写不下」。这短短一句话引发了长达三百六十余年的数学探索，吸引了无数数学家倾注毕生心血试图填补这片「空白」。1908年，一位德国实业家悬赏十万德国金马克（相当于今天数百万美元）征集正确证明，仅第一年就收到六百二十份错误证明，可见此题之深不可测。
Andrew Wiles的划时代证明与验证之路
1993年6月，英国数学家安德鲁·怀尔斯在连续三天的系列讲座中公布了他认为是第一个正确的费马大定理证明。然而在为期两个月的高强度同行审查中，审稿人发现了证明中一个重大缺口。怀尔斯随后花了近一年时间修补缺陷，最终在1995年以一篇长达一百二十九页的论文成功完成了证明，这一成果也被公认为二十世纪数学的重大突破之一。然而，即便证明已发表三十年，人工审阅如此复杂的逻辑链条仍然充满挑战——单一推理环节的疏漏就可能动摇后续所有推论的根基。荷兰计算机科学家扬·贝格斯特拉在二十一世纪初提出将怀尔斯的证明进行形式化的想法，即把数学推理转换为计算机可以自动校验的格式。
Claude的11天自主形式化之旅
Anthropic研究员、哥伦比亚大学自动形式化工具研究组的彭天怡决定测试Claude能否在费马大定理形式化方面取得进展。结果远超预期——在11天高度自主的运行过程中，Claude完成了费马大定理的首个端到端、经机器全面验证的证明。整个过程共编写了约一千三百万行Lean证明助手代码，并证明了两万九千五百条中间定理。帝国理工学院的凯文·巴扎德教授此前曾在2024年启动了一项多社区协作项目，旨在利用Lean完成这一形式化工作。收到Anthropic提供的证明后，巴扎德评价道：「这一非凡的自动形式化成就仅用了11天，它仅在数学公理的假设下证明了费马大定理，过程中涵盖了代数、调和分析、几何与数论的形式化工作。」
自动形式化对数学研究的深远意义
Anthropic指出，与近期AI在黎曼假设上的新数学研究不同，这次工作的核心突破在于验证本身——如同用计算器校验数学计算一样检验一个数学证明的正确性。传统的数学证明审阅是一个漫长而高风险的过程：理解一个新结果到足以确信其正确性可能需要数月乃至数年的持续工作。随着AI产出的数学成果日益增长，便捷的形式化验证能力将大幅减轻评估新结果的负担。Anthropic表示希望这能让维护数学知识体系的可信度变得更加容易，而非更加困难。
形式化验证的技术架构与社区遗产
Lean是一个交互式定理证明器，已被全球数学家和计算机科学家广泛采用来编写可机器检查的数学证明。凯文·巴扎德领导的费马大定理形式化项目自2024年启动以来，汇集了多个机构的研究人员，逐步发展出编码复杂证明所需的方法论。此次Claude能在短时间内独立完成这一形式化任务，一方面展示了AI辅助严格数学推理的巨大潜力，另一方面也证明了社区多年来在Lean中建立的工具链和中间库已足够成熟，能够支撑如此复杂项目的自动执行。
从十万马克悬赏到AI自主证明
回溯费马大定理的历程，从费马1637年写下的页边笔记，到1908年十万金马克的世纪悬赏，再到怀尔斯1995年划时代的证明，直到今天Claude用11天生成第一个端到端机器验证版本，这条漫长的道路折射出人类在追求确定性与严格性上的不懈努力。巴扎德教授强调，该证明中的自动形式化产物已「足够健壮，可以作为后续工作的基础」，证明本身具有多层次的逻辑结构。这意味着AI形式化不再停留在玩具演示阶段，而是开始进入可实际复用的工程层面，为数学研究开辟全新的合作范式。
从更宏观的视角来看，此项成果标志着AI在科学验证领域的重大进展。数学作为形式推理最严谨的学科，一直是衡量AI推理能力的终极标尺之一。Claude在近乎无人值守状态下完成如此规模的形式化工作，体现了大型语言模型在结构化推理上的能力飞跃，也为数学家与AI建立更紧密的协作关系奠定基础。未来数学论文或许都能附带机器可检查的Lean证明，让人机共同守护数学知识体系的可靠性。