GPT-6 Astra 已全面推送，Claude 证明了费马大定理
浮之静 · 人工智能
原创 lencx 2026-09-05 09:32 上海 当 AI 疯狂在卷时，人类又该何去何从... Astra 全面推送 GPT-6 Astra 现已全面推送，Plus 用户也可用（ GPT-6 Astra：从智能模型到执行系统 ）。昨天 Sam 还在吐槽 “rollout 过程混乱，搞砸了”，今天 Tibo 就夸团队做的好 “系统比预期的更具可扩展”... 如果 Astra 模型不可见，可以尝试更新 Codex 应用，然后再重启或重新登录账号 。Astra 使用限额官方文档没给固定“消息条数”，只给了每 5 小时本地消息数的估算范围。了解更多 Pricing docs [1] 需要注意： 这些是估算区间，不是保证条数。长任务、大上下文、高推理强度、工具调用和检索都会更快消耗额度。 本地消息和云端聊天共享套餐额度，而且还可能有额外的周限额。 同一套餐下，GPT‑6 可完成的消息数大约只有 GPT‑5.6 Sol 的一半。 按 credits 计费时，每 100 万 tokens：输入 250 credits、缓存输入 25 credits、输出 1,250 credits；Fast 模式消耗为标准模式的 2.5 倍。 Plus/Pro 达到包含额度后可购买 credits；也可以用 API Key 继续运行本地任务，另按 API 计费。 最终以账户的 Usage Dashboard 和实际重置时间为准。 Claude 证明 据 Anthropic 介绍（ Formalizing Fermat's Last Theorem [2] ），数十个 Claude 智能体在少量人类指导下，用 11 天完成了费马大定理的形式化。过程中共生成 30,300 个机器可检验的定理证明，约 29,500 个进入最终证明；公开仓库（ anthropics/fermats-last-theorem [3] ）的精确数字是 29,511 个。整个项目约 1,350 万行 Lean 代码，超过其所依赖版本 Mathlib 的 5 倍，涉及代数、调和分析、几何和数论等多个领域。 Claude 的形式化遵循 Darmon、Diamond 和 Taylor 对 Wiles 证明的简化阐述，其背后汇集了 Frey、Serre、Ribet、Mazur、Langlands和 Tunnell 等数学家的工作。整条路线采用反证法：从一个假设中的反例构造 Frey 曲线，再结合不可约性、模性与降层等关键结果导出矛盾。Claude 将这套既有数学论证落实为完整的 Lean 定义、中间定理和机器可检查的证明。按照 Anthropic 自己的说法，这次成果的新意主要在于首次完成端到端的计算机验证，而非提出新的费马大定理证明。 Anthropic 称，其中包含许多此前尚未形式化的具体结果，但没有公布逐项的前人成果对照，因此不能笼统地说这些数学领域此前都没有被形式化。30,300 个定理也不等于同等数量的新数学发现，其中包含大量辅助引理、基础设施和已有结果的形式化。 这套证明很难靠人力逐行审阅。仓库提供了约 390 MB 的离线网页，为 29,511 个定理和 1,450 个定义模块展示引用关系与依赖图，但英文摘要也是机器生成的，最终仍以 Lean 陈述为准。完整复验的门槛同样很高：源码构建峰值内存约 153 GB；Comparator 检查接近 15 小时，峰值约 230 GB，项目建议准备 300 GB 内存。因此，源码公开、流程可重复，并不意味着普通数学家可以轻松完成独立复验。 Lean 内核负责检查提交的证明能否在既定定义和公理下成立。Comparator 是一套验证流程，负责核对可信命题、限制公理并调用 Lean 官方内核重放证明。项目随后还单独使用 Nanoda 对导出的证明环境进行了第二轮检查。Nanoda 是用 Rust 独立实现的 Lean 内核，与官方内核属于两套不同的软件实现，可以降低单一内核出错的风险。 不过，交叉检查仍无法彻底排除共同缺陷、导出链路错误或可信命题写错的可能。仓库目前也没有公开完整的验证日志或验证 CI，评审状态仍是 self-assessed。这些情况不会直接说明证明有错，但意味着独立验证仍有继续完善的空间。 Anthropic 还提到，早期失败尝试留下的成果约占最终非模板代码的 7%。这说明中间成果得到了复用，不能直接视为代码质量问题。更现实的疑问来自仓库自己的定位：源码主要为机器检查而写，名称由机器生成、注释很少，而且项目暂不维护。它能否进一步整理成数学家容易理解、社区可以长期复用的知识库，仍有待观察。 至于 AI 能否由此证明更多定理，答案很可能是肯定的；能否发现人类未知且真正重要的新数学，目前还没有答案。Lean 可以确认推导是