GPT-6 Astra全面推送 Claude完成费马大定理形式化
当AI技术迭代速度不断加快，各类模型与应用持续推陈出新，我们该如何跟上技术发展的节奏，同时确保这些成果的可信度？近期AI领域的两项进展，恰好让这个问题变得更加迫切。
Claude完成费马大定理形式化验证
据相关团队介绍，数十个Claude智能体在少量人类指导下，仅用11天就完成了费马大定理的形式化验证。整个过程生成了30300个可由机器检验的定理证明，其中29511个最终纳入正式证明流程，对应的公开仓库包含约1350万行Lean代码，是其所依赖的Mathlib版本的5倍以上，覆盖了代数、调和分析、几何与数论等多个数学领域。
Claude的形式化工作基于Darmon、Diamond和Taylor对怀尔斯证明的简化阐述，整合了Frey、Serre、Ribet、Mazur、Langlands和Tunnell等多位数学家的研究成果。整个证明路径采用反证法：通过假设存在反例构造Frey曲线，结合不可约性、模性与降层等关键结论推导出矛盾。Claude将这套完整的数学论证转化为标准的Lean定义、中间定理和可机器检查的证明。相关团队表示，此次成果的核心意义在于首次完成了费马大定理证明的端到端计算机验证，而非提出全新的证明方法。
该项目包含了大量此前未被形式化的具体数学结果，但团队并未公布与前人成果的逐项对比，因此无法笼统判定这些数学领域此前都未被形式化。30300个定理证明也并非全部都是全新的数学发现，其中包含大量辅助引理、基础设施代码和已有结论的形式化工作。
这份证明很难通过人力逐行审阅。公开仓库提供了约390MB的离线网页，用于展示29511个定理和1450个定义模块的引用关系与依赖图，但所有英文摘要均由机器生成，最终的验证仍需以Lean代码的陈述为准。完整复验的门槛极高：源码构建的峰值内存约为153GB，Comparator检查流程耗时接近15小时，峰值内存约230GB，项目建议用户准备至少300GB的内存空间。因此，尽管源码公开且流程可复现，但普通数学家也很难独立完成完整的复验工作。
Lean内核负责检查提交的证明是否符合既定的定义和公理。Comparator是一套验证流程，用于核对可信命题、限制公理范围并调用Lean官方内核重放证明。项目还使用Nanoda进行了第二轮独立检查，Nanoda是用Rust独立实现的Lean内核，与官方内核属于两套不同的软件实现，能够降低单一内核出现错误的风险。不过，这种交叉检查仍无法完全排除共同缺陷、导出链路错误或可信命题编写失误的可能。仓库目前并未公开完整的验证日志或持续集成验证流程，评审状态仍为自我评估。这些情况并不直接证明证明存在错误，但也意味着独立验证仍有进一步完善的空间。
相关团队提到，早期失败尝试留下的成果约占最终非模板代码的7%，这说明中间成果得到了复用，不能直接视为代码质量问题。不过该仓库也存在一些现实局限：源码主要为机器检查而编写，模块名称由机器生成，注释极少，且项目目前暂不维护。它能否被进一步整理为数学家易于理解、社区可以长期复用的知识库，仍有待观察。
AI能否借助这类工具证明更多定理？答案大概率是肯定的。但AI能否发现人类未知且真正有价值的新数学成果，目前还没有明确答案。Lean可以确认推导过程是否成立，但无法判断一个结论是否新颖、重要或值得研究。将这项成果视为纯粹的噱头会低估其价值，但它距离真正能够提出优质问题、发现全新数学结构的“AI数学家”，仍有很长的一段路要走。
GPT-6 Astra全面推送
GPT-6 Astra现已全面开放推送，付费用户均可使用。此前团队成员曾吐槽推送过程存在混乱，不过后续团队也对系统的扩展性给出了积极反馈，称其表现超出预期。如果用户无法看到该模型，可以尝试更新Codex应用后重启或重新登录账号。
官方并未给出固定的消息条数限制，仅提供了每5小时本地消息数的估算范围，同时有几点需要注意：
- 该估算区间并非保证额度，长任务、大上下文场景、高推理强度的操作，以及工具调用和检索操作都会更快消耗配额。
- 本地消息和云端聊天共享套餐额度，部分套餐还可能存在额外的周限额。
- 相同套餐下，GPT-6可处理的消息数大约仅为GPT-5.6 Sol的一半。
- 按积分计费的规则为：每100万tokens，输入消耗250积分，缓存输入消耗25积分，输出消耗1250积分；Fast模式的消耗为标准模式的2.5倍。
- 付费套餐用户在套餐额度用完后，可以购买额外积分；也可以使用API Key运行本地任务，按照API计费标准另行结算。
- 最终额度以账户的使用仪表板和实际重置时间为准。
更多详情可查阅定价文档。
结语
Claude完成费马大定理的形式化验证，将一个现实问题摆在了所有人面前：当AI生成代码和证明的速度快到人类无法逐行审阅时，我们该如何验证这些成果的可信度？AI模型的能力还会持续增强，但它最终能走多远，取决于验证能力能否同步跟上。无论技术成果多么惊人，我们最终都要回到一个最基本的问题：我们为什么要相信它？
参考文献
[1] https://learn.chatgpt.com/docs/pricing
[2] https://www.anthropic.com/research/formalizing-fermats-last-theorem
