2026年9月4日，Anthropic公布Claude对费马大定理的完整形式化成果；9月7日，《自然》新闻栏目对此进行了独立报道。这项工作不是重新发现费马大定理的新证明，而是把既有数学论证转化为Lean可以逐步检查的形式化证明。事件真正提出的新问题是：当AI能够大规模生成可验证代码时，机器核验是否等于同行复核，成果又应当署给谁？
形式化验证解决了什么，又没有解决什么
Anthropic称，Claude在约11天内生成约1300万行Lean代码，最终证明使用了29511个定理，并且只依赖Lean的三项标准公理。项目还使用comparator和nanoda进行外部检查。帝国理工学院数学家Kevin Buzzard审阅后，将其评价为重要的自动形式化成果。《自然》于2026年9月7日将其称为数学领域的一项重要里程碑。上述信息说明，成果至少具备公开程序、可重复运行和接受外部检查的基础。
但Lean检查通过只能回答：在给定公理、定义、依赖库和形式化语句下，推导是否成立。它不会自动判断目标定理是否表述正确，也不会解释证明为何重要、是否真正对应人类论文中的全部数学含义。Anthropic公开的技术材料还明确表示，大部分代码由机器生成，目前并不符合Mathlib通常要求的精炼程度。因此，“机器已验证”不能被简化为“数学界已完成同行评议”。
同行复核应采用三层机制
第一层：复现机器检查
发布方应固定代码版本、Lean版本、Mathlib依赖、构建脚本和校验值，让第三方能够在独立环境中重新编译。复核者不仅要看到绿色的通过标记，还应确认最终定理的准确表述、所用公理、是否存在未完成占位符，以及依赖项是否被悄然替换。Anthropic此次公开代码并使用两种外部检查器，是可借鉴的起点，但复现报告仍应由无利益关联的机构分别发布。
第二层：审查数学对应关系
专家需要抽查从自然语言证明到形式化定义的映射，特别是关键对象、边界条件和深层定理的特殊版本。Claude的成果沿用了Wiles及Taylor与Wiles的证明路线，并参考Darmon、Diamond和Taylor的阐释，同时建立在Mathlib、帝国理工学院FLT项目和flt-regular项目之上。形式系统内部没有矛盾，不代表转译过程没有选错命题。同行评审仍须回答“机器证明的是不是我们想证明的那个命题”。
第三层：评价原创性与学术意义
此次核心创新在自动形式化规模和协作工程，而不是提出费马大定理的新数学证明。论坛讨论和媒体标题应明确使用“形式化”“计算机检查”或“自动转译”等限定词，避免写成“Claude首次证明费马大定理”。这既符合信息真实性底线，也能防止夸大产品能力、误导公众或不当削弱既有数学家的贡献。
署名责任不能交给模型承担
AI系统不具备承担纠错、利益冲突披露和研究伦理责任的现实能力，因此不宜作为独立作者。较稳妥的做法是由能够解释流程、回应质疑并负责修订的人类研究者署名；Claude、Prove2Me、Lean及具体模型版本则在方法、致谢和贡献声明中完整列出。
贡献声明至少应区分四类角色：提出目标和配置流程的人，开发多智能体平台与验证工具的人，提供既有形式化代码和数学蓝图的社区贡献者，以及负责独立审查和复现的人。对于从外部项目改写的文件，应逐项保留许可证、提交历史和原作者信息。Anthropic的技术材料称有106个文件改编自帝国理工学院FLT项目及flt-regular，这说明依赖链披露不是礼节，而是确定知识来源和责任边界的必要条件。
人类署名者还应承担三项持续责任：发现错误后发布更正和版本记录；公开计算资源、模型权限及潜在利益冲突；在宣传中区分公司陈述、机器验证结果和独立专家意见。不能一方面把成功归功于AI，另一方面在出现错误或权属争议时宣称“这是模型自主生成”。
论坛发布如何守住真实性与合法权益底线
依据《互联网信息服务管理办法》关于信息内容合法性的要求，以及“七条底线”中的法律法规、公民合法权益、社会公共秩序、道德风尚和信息真实性原则，相关讨论应避免未经证实的数字、攻击数学家能力、虚构专家背书或把企业公告包装成学界共识。引用公开仓库时还要遵守许可证，不应大段复制论文、代码说明或他人评价后冒充原创。
- 标题标注：使用“形式化并经机器检查”，不用“AI独立攻克费马大定理”。
- 资料分级：将企业公告、技术文档、代码仓库、专家评论和媒体报道分别标识。
- 证据留存：保留发布日期、版本号、提交记录、构建日志和复现环境。
- 责任到人：由具名研究者或机构对目标定义、资料使用、结果解释和后续更正负责。
- 审慎表述：在独立复现范围有限时，明确写出“已通过形式系统检查”而不是“所有数学细节均已获得学界确认”。
总结
Claude形式化费马大定理展示了AI压缩大型数学工程周期的潜力，但可信科研不能只靠一次编译通过。可持续的制度应当把机器核验、人类数学审查、独立复现和责任署名连接起来：模型负责生成与辅助检查，形式系统负责验证推导，人类作者负责解释、披露和纠错，学术共同体负责判断原创性与意义。只有这四个环节同时存在，AI数学证明才可能从企业展示转化为可积累、可追责的公共知识。
事件及资料日期：
2026年9月4日，Anthropic发布Claude形式化费马大定理的官方说明，并公开说明运行周期、代码规模、验证方法及既有项目依赖。
2026年9月7日，《自然》发布独立新闻报道，核验了事件性质、发布时间和约1300万行计算机检查证明等核心信息。
Anthropic同步发布的技术材料记录了证明时间线、29511个定理、两种外部检查器及既有代码来源。
内容发布规范参考现行《互联网信息服务管理办法》有关信息合法性和禁止传播违法内容的规定。
