AI 行业快讯（2026-10-28）：数学巨著完成 Lean 形式化、Apple M6 登场、Anthropic 上市代码「ANT」

1. 有限简单群分类在 Lean 中形式化：4310 万行代码复核了百年人类证明（HN 171 分）

AxiomMath 主导的项目宣布完成有限简单群分类（Classification of Finite Simple Groups, CFSG）在 Lean 证明助手中的形式化——这是群论史上最庞大的集体成果：跨越数十年、约百位数学家、上千页期刊论文的证明，如今每一步逻辑都由 Lean 内核机器校验，规模达 4310 万行 Lean 代码、205 万条声明、715 篇论文与书籍、100 个里程碑。

最值得关注的不是数字而是副产品：形式化过程中在已发表的「非平衡群定理」论证里发现了一处错误，并用 Solomon 关于极大 2-群的理论给出替代证明路径，另成 35 页论文（Hexagon 2610.00575）。项目由 Dean Cureton、Vasily Ilin、Bhavik Mehta、Niels Voss 与约 30 位贡献者完成，首席研究者是 Ken Ono。

这与我们近一个月的观察形成闭环：陶哲轩的「Math 2.0」预言形式化是数学 AI 的关键基础设施；OpenAI 用模型攻克开放问题并附 Lean 证明；Claude 破解 NIST 曲线种子悬案。「AI 产出 + 形式化验证」正在成为数学研究的默认工作流，而这次的形式化还证明了一件更实际的事——机器校验不只能验收 AI 的结论，也能找出人类论文里的错误。

2. Apple 发布 M6 芯片与 14 英寸 MacBook Pro（10/27）

Apple 官方新闻稿确认：全新 M6 芯片（12 核 CPU，官方称「世界最快的 CPU 单核」；12 核 GPU，图形性能较 M5 快最多 30%，AI 负载快最多 25%）首发于 14 英寸 MacBook Pro，续航达 24 小时，另有配套的新 iMac。

对做本地 AI 的团队，这是今年最实用的一块硬件之一：单核性能与端侧 AI 吞吐同时提升，直接关系到「桌面级模型」（如 Meta Muse Spark Open 在两台 M5 Ultra 上跑 816B）这条本地化路线的可行性——M5 Ultra → M6 的代际升级意味着本地前沿模型的部署门槛继续下移。Apple 同日发布 iMac 与 MacBook Pro 两款产品线，显示 M6 是全线换代的开始。

3. Anthropic IPO 细节确认：纳斯达克代码「ANT」，高盛与摩根士丹利承销（10/26 官方公告）

Anthropic 官方公告页披露了 S-1 的具体安排：A 股代码将在纳斯达克全球精选市场挂牌，代码为「ANT」，承销方为高盛与摩根士丹利，发行股数与价格区间尚未确定——也就是说，估值 2 万亿美元的目标尚未落定，最终定价要等路演。此前我们已报道过招股书里的财务面：2026 上半年营收 163 亿美元、三季度单季 168 亿、巨额账面亏损中约 720 亿为非现金项。

给企业采购方的实操提醒：一旦 Anthropic 完成上市，其财务状况与经营连续性将有季度公开披露可供核对——供应商风险的可见度会再上一个台阶；同时也请留意，IPO 前后的定价与商业策略调整（如我们此前报道的降价潮）可能影响你们的服务条款。

综合 axiommath.ai、Axios/Ars Technica、Apple Newsroom、Anthropic 官方公告与 Hacker News 社区信号。