Anthropic用Claude形式化证明费马大定理

Anthropic宣布，其AI模型Claude成功将数学界著名的费马大定理证明形式化，生成了由1300万行Lean代码构成的计算机可验证版本。这一成果将原本预计需要数学家数年才能完成的工作压缩至11天，被认为是AI在复杂科学推理领域的一次重要突破。 费马大定理由法国数学家皮埃尔·德·费马于1637年提出，直到1995年才由英国数学家安德鲁·怀尔斯给出完整证明，该证明长达129页，当时经过了数月的严格审查才被学界接受。所谓“形式化”，是指将人类书写的数学证明转换成计算机能够自动验证的代码语言Lean，从而排除人为笔误或逻辑疏漏的可能，也便于全球数学家在此基础上共享和推进研究。由于原始证明行文简略，且各论证环节高度依赖前后文，形式化过程向来极其繁琐，此前数学界普遍认为完成这项工作需要数年时间。 Anthropic表示，其内部研究模型在人类仅提供少量高层级指引的情况下，自动生成了数十个AI代理协同工作，累计输出60亿个token，并在此过程中证明了29500个中间定理。值得注意的是，项目初期并不顺利，关键突破发生在团队为Claude接入开源工具Prove2Me之后，该工具帮助AI代理在长流程任务中更高效地判断下一步操作，同时降低了推理成本。Anthropic将此次成功部分归功于数学家凯文·巴扎德此前的研究成果，巴扎德本人也评论称，AI形式化产物已具备足够的稳健性，可以支撑后续多层级的数学构建。 这一成果紧随Anthropic上月公布的另一项进展而来，当时Claude在黎曼zeta函数的研究中发现了新信息，该函数是数学界最著名难题之一黎曼猜想的焦点。与此同时，竞争对手OpenAI也在利用其最新Astra模型解决多个厄尔多斯问题，并缩小了理论计算机科学中若干开放问题的范围。业界分析认为，AI在数学研究中的应用正从辅助计算走向自主推理，未来或能帮助人类在数论、几何等基础科学领域发现新的定理和证明路径。