Anthropic于近日宣布，旗下AI模型在基本自主运行11天后，成功完成了对费马大定理的首个端到端、经过计算机检查的Lean形式化证明。
在这一过程中，Claude生成了约1300万行Lean代码，并证明了约3.03万个定理，其中约2.95万个中间定理最终被纳入费马大定理的完整证明。整个证明由Lean完成检查，仅使用了Lean的3条标准公理。这项工作的目标是将英国数学家安德鲁·怀尔斯于1995年完成的费马大定理证明进行形式化。Anthropic此前曾预计费马大定理的形式化工作可能需要数年时间。人类研究人员提供的数学输入主要是少量高层次指令，例如确定某些数学对象或定理的优先级，具体证明过程则主要由Claude完成。此次项目的完整Lean证明已经公开在GitHub上。
这条信息对你有帮助吗？