AI攻克十项数学开放难题全解析：非sofic群、球堆积指数与Lean形式化验证的完整拆解

本文由 辛梓煜@词元2号站（www.ciyuanerhao.com）撰写，转载请注明出处。

快速摘要

2026年8月1日，OpenAI 公开了一份249页的手稿，宣布其未发布的下一代模型 Astra 在十个"至少十年没有主要进展"的数学与理论计算机科学开放问题上给出了新结果。十项里最硬的三项是：首次显式构造出非sofic群（终结Gromov自1999年提出的核心问题）、证伪Connes刚性猜想、以及自1978年以来首次推进高维球堆积的一般指数（从 0.59905576… 推到 0.6044…）。每一项都附带 Lean 4 形式化证书，机器可独立核验。全部十道题的求解token开销按官方口径折算约2000美元。

这件事之所以值得写一篇长文拆开讲，不只是因为"AI很强"这四个字。真正的分水岭在于三个词：开放问题、形式化证书、可复核。以前模型刷的是有标准答案的题库，现在它交出来的是没有人知道答案的命题，而且交付形态是机器能一行一行查的证明脚本，而不是一段读起来很顺的自然语言。

但同样重要的是另一面：形式化证书只能保证"证明过程无误"，保证不了"这条被形式化的命题，就是数学家心里那个开放问题"。这两件事之间的缝隙，恰恰是接下来几周同行审读要盯的地方。国际数学联盟背书的《莱顿宣言》在两个月前刚刚划下了这条线。

想看完整拆解——十项结果分别是什么、Astra到底用了什么路子、Lean验的是什么不验什么、2000美元这个数字该怎么读、以及普通人怎么自己动手复核一遍——往下翻。

一、事件全貌：一份249页手稿，把讨论的前提改了

1.1 8月1日到底发生了什么

先把事实按顺序摆清楚，不加修饰。

2026年8月1日，OpenAI 在官网发布了一篇标题很朴素的公告：《数学与理论计算机科学的十项进展》。配套物料一共四件：

• 一份249页的手稿 PDF，把十项结果各自写成了独立章节；
• 一份"推理过程走查"文档，公开了模型在每道题上的思考轨迹节选；
• 一个 GitHub 仓库 openai/ten-proofs，装着十项结果各自的 Lean 4 形式化脚本；
• 一段关于署名与责任归属的说明。

公告里最关键的一句话是身份确认：这些结果由 Astra 的一个内部版本产出，Astra 是 OpenAI 的"下一代主力模型"。这也是 OpenAI 第一次在官方渠道确认 Astra 这个名字。

在这之前，Astra 只在传闻层面存在。行业媒体的报道说它是一个新的模型家族，与 OpenAI 现有的 Sol、Terra、Luna 三条线并列，设计目标是让多个智能体协同处理需要数小时甚至数天的长时程任务。它最终会以 GPT-6 的名义发布，还是作为 GPT-5 系列的一个变体（比如 GPT-5.7）发布，公司内部还没定，发布日期也没有。奥特曼在此之前已经把 Astra 演示给了华盛顿的政策制定者，包括一批美国参议员。

1.2 这不是第一次，但和上一次不一样

时间往回倒三个月。2026年5月，OpenAI 公布过一次：一个未发布的推理模型证伪了埃尔德什（Paul Erdős）1946年提出的平面单位距离猜想——一个已经悬了八十年的离散几何问题。当时的反响就已经不小，菲尔兹奖得主 Tim Gowers 说过，那份证明他会毫不犹豫地推荐给《数学年刊》。

现在确认了，5月那个"未发布模型"，就是 Astra。

但这次和上次有三个结构性差别，我把它列成表，比较直观：

第三行是关键。从"你读一读，看对不对"变成了"你跑一遍，机器告诉你对不对"，这是审阅成本量级上的变化。曼彻斯特大学的数学家 Thomas Bloom（他维护着 erdosproblems.com 这个埃尔德什问题库）在社交平台上说，就构造本身而言，这批结果比之前的单位距离反例分量更重。

1.3 Astra 是个什么东西

关于 Astra 本身，公开信息其实不多，但有几点可以确定：

它是"下一代主力模型"，还没发布。 OpenAI 用的措辞是 next major model，并且明确说这次做题的是"内部版本"。也就是说，外面的人现在拿不到这个模型，无法自己重跑一遍。

它被设计成长时程、多智能体协作的形态。 这一点从做题方式上能看出端倪——解一个研究级问题不是一次问答能完成的，需要反复试错、回退、换路线。行业报道提到 Astra 的设计目标就是让多个 agent 协同啃数小时到数天的任务。

它的成本口径参照的是 Sol API 价格。 官方说全部十道题"找到解法"所消耗的 token，按 Sol 的 API 价格折算大约2000美元。注意这句话的限定词，第九章我会专门拆这个数字。

我自己盯这条线盯了一年多，感觉最微妙的一点是：这次 OpenAI 的公告口吻明显收敛了。没有堆形容词，甚至专门写了一整段谈"对数学共同体的责任"，主动引用了两个月前发布的《莱顿宣言》，并且明确表态——由AI系统完整生成的证明，如果署人类作者，会同时误述系统的贡献和人类智力工作的性质。这段话的分量，比"我们又刷新了一个基准"大得多。

二、先把"开放难题"这四个字说清楚

这一章可能是全文最重要的一章。因为如果不先把"研究级开放问题"和"有答案的难题"分开，后面所有讨论都会跑偏。

2.1 竞赛题和研究题，差在哪

很多人对"AI做数学"的印象还停留在两年前：模型解奥数题、拿IMO金牌水平。那类任务有一个共同特征——答案存在，而且出题人知道答案。模型要做的是在有限步骤内找到一条已经被验证过的路径。这本质上还是"搜索 + 模式匹配"能覆盖的范畴，哪怕搜索空间很大。

研究级开放问题完全不是这个结构。它的特征是：

• 没有人知道答案是什么，甚至不知道答案存不存在；
• 不知道该往哪个方向找，可能需要引入一个此前完全不在这个领域视野里的工具；
• 失败没有反馈信号。做错一道竞赛题，对答案就知道错了；在开放问题上走错方向，可能几个月后才发现死路。

打个不太严谨但好懂的比方：竞赛题像是走一座已经修好的迷宫，出口确实存在，只是路绕；开放问题像是站在一片没有地图的荒野上，你甚至不确定前面有没有路，也不确定终点在不在这个方向。

Astra 这次交出的是后者。它给出的是此前不存在的论证——不是复述文献里的某个技巧，而是提出一条新路径，然后接受形式化系统的逐步检查。这就是所谓"进入研究无人区"。

2.2 "十年无进展"是个光谱，不是一个标签

这一点我必须写出来，因为它是理解这次事件的分水岭，也是最容易被忽略的地方。

OpenAI 的措辞是：这十个问题"至少十年没有在主要结果上取得进展，多数情况下远不止十年"。这句话字面上没问题，但**"开放"是一个光谱，不是一个二值标签**。

有些问题开放，是因为它真的难——几代顶尖数学家反复冲击，工具用尽，仍然卡死。非sofic群和球堆积指数属于这一类，前者27年无人构造出反例，后者的指数48年纹丝不动。

有些问题开放，是因为它坐在一个没人有理由去的角落。不是攻不下，而是没人去攻——领域太窄、没有下游应用、没有人拿它当博士课题。这类问题一旦被认真看一眼，可能几周就解决了。

"十年没进展"这个描述，对上面两类同时成立。而这两类的意义天差地别。

我的判断是（辛梓煜@词元二号站的个人看法，不代表任何权威）：接下来几周，做这些方向的数学家会把这十项自然地分成两堆——一小堆是真正让人意外的，另外几项会被专业人士描述为"够得着但没人去够"。这两堆都是实打实的进展，但只有前一堆撑得起"分水岭"这个框架。

不过话说回来，这两类的分野并不削弱这件事本身。因为哪怕全都属于"够得着但没人去够"，那也意味着：一个模型现在能自主识别出哪些角落值得去够，并且在够到之后能把论证写完整。这个能力，本身就是新的。

2.3 一个必须先接受的前提：多数人看不懂原文

我不打算装。这249页里的绝大部分内容，包括我自己在内的绝大多数读者是读不下来的。第一章那些Mellin变换、鞍点估计、Poisson核外推，是泛函分析和调和分析里相当专门的技术。

所以这篇文章的定位不是"带你读懂证明"，而是三件事：

1. 把每项结果在说什么讲清楚，用白话；
2. 把 Astra 走的是哪条路讲清楚，哪怕只到策略层面；
3. 把这件事该怎么判断真伪讲清楚——尤其是形式化验证的能力边界。

第三点其实最有实用价值。因为在接下来很长一段时间里，我们会不断遇到"AI证明了某某"的新闻，而能不能自己判断一条这样的新闻靠不靠谱，是一项可以迁移的能力。这个判断框架，我放在第八章和第十章讲。

先说个前置结论，你可以带着往下读：看到"AI证明了X"，第一个要问的不是"证明对不对"，而是"被证明的X，是不是原来那个X"。

三、十项成果全景：先看表，再分类

3.1 一张表看懂十项结果

我按官方手稿的章节顺序整理了这张表。这是全文的骨架，后面几章都是在这张表上做展开。

看这张表的时候有几个细节值得留意。

第一，覆盖面异常宽。 这十项横跨了纯数学（群论、算子代数、凸几何、组合）和理论计算机科学（电路复杂度、量子复杂度、格问题）两大块。这两块虽然有交叉，但日常使用的工具箱差别很大。一个人同时在这么多方向上做出研究级贡献，几乎不可能。

第二，第1项和第2项其实是一件事的两面。 手稿里写明了：第2章球面码构造在 (s\to 1) 的极限下，会重新导出第1章的球堆积指数。也就是说，同一个数学事实被两条独立的路子各走了一遍。这种"互相印证"的结构，在可信度上是加分项。

第三，埃尔德什问题被解决了三个。 第9项对应183号，第10项一次对应146号和180号。埃尔德什问题库是组合数学里一个公开的悬赏清单，每一条都有明确编号和状态，谁解了、什么时候解的一目了然。这意味着这三项的"是否真的开放"这件事，几乎没有争议空间。

3.2 按"是构造还是证明"重新分类

上面那张表是按领域分的。我觉得还有一种分法更能看出 Astra 的能力结构——按数学动作的类型分。

第一类：造反例（构造性证伪），包括第3、4、10项。

这类任务的形态是：有一个大家相信为真的猜想，你要造出一个具体的对象，把它打掉。它的难点在于目标对象的形状完全未知，你不知道要造的东西长什么样，只知道它必须同时满足一堆互相拉扯的条件。

这一类是 Astra 表现最亮眼的地方。非sofic群、Connes反例、两个极值图论反例，全部属于此。而且第4项特别狠——它不是造出一个反例交差，而是造出了无限多个两两不同构的群，它们共享同一个冯·诺依曼代数。

第二类：把界推进去（定量改进），包括第1、2、5、7、9项。

这类任务的形态是：某个量的上界或下界卡在某个数值上很多年，你要把它往前推。难点不在于"想到"，而在于精确控制每一步的损耗。这类工作在分析和复杂性理论里很典型，往往需要非常克制、非常技术性的估计链条。

第1项和第2项在这一类里最狠，因为它们改的是指数，不是常数因子。此前几十年间也有人改进过这些界，但改的都是低阶因子；指数纹丝不动。

第三类：证明一个此前只能猜的定理，包括第6、8项。

Ehrhart 体积猜想给出的是一个精确的、漂亮的闭式：((n+1)^n/n!)。量子平行重复则是把经典复杂性理论里一条基础原理，推广到了此前只有特例结果的量子纠缠情形。

我把这三类画成一张图，方便记：

graph TD
    A[Astra 十项结果] --> B[构造反例]
    A --> C[定量推进边界]
    A --> D[证明新定理]
    B --> B1["#3 非sofic群"]
    B --> B2["#4 Connes刚性猜想"]
    B --> B3["#10 紧致性/退化性猜想"]
    C --> C1["#1 球堆积指数"]
    C --> C2["#2 二进制/球面码"]
    C --> C3["#5 permanent电路下界"]
    C --> C4["#7 CVP近似难度"]
    C --> C5["#9 多色拉姆齐数下界"]
    D --> D1["#6 量子平行重复"]
    D --> D2["#8 Ehrhart体积猜想"]

这三类里，构造反例这一类的信号最强。因为定量推进和定理证明多少还能靠"沿着已有技术路线再压一层"，而造一个从来没人见过的数学对象，需要的是另一种东西——一种在结构空间里找方向的能力。

3.3 一个容易被误读的点

网上流传的一些中文版本里，把第3项写成了"构造出无限有限呈现的非sofic群"。这句话读起来很怪，因为它其实是把第3项和第4项揉在一起了。

按官方手稿的原始表述：第3项是"构造出一个显式的非sofic群"——一个，不是无限多个；第4项才是"构造出无限多个两两不同构的性质(T)群"。"无限多个"这个定语属于 Connes 那一项。

还有一处，流传版本说第3项用的是"Kun-Thom扩展图理论"糅合"汤普森群V"。手稿摘要写得很清楚：用的是性质(T)扩张图（property-(T) expanders）和二元 Leavitt 代数（binary Leavitt algebra）。这两个东西和汤普森群V不是一回事。

我把这两处专门拎出来，不是为了挑刺。而是因为这类信息在传播链条上每转一手就会走样一点，而数学结论恰恰是最不能走样的那种信息。往下读的时候，如果你在别处看到和本文不一致的说法，建议以官方手稿为准。

四、拆解一：非sofic群——27年悬案，和"有限逼近"的边界

这是十项里公认最重的一项，也是最值得花笔墨讲的。

4.1 群是什么，先用一句话过

"群"这个词在数学里指的是一套对称性的集合。你可以想象一个正方形，把它旋转90度、180度、270度、360度，或者沿对角线翻转——所有这些"做完之后看起来跟原来一样"的操作，合起来就构成一个群。

群的核心信息藏在乘法表里：做完操作A再做操作B，等于做了哪个操作？这张表把群的全部结构编码了进去。

有限群的乘法表是有限大的，能整张写出来。无限群——比如整数在加法下构成的群——乘法表是无限大的，写不完。这就带来一个自然的问题：无限群能不能用有限的东西去逼近？

4.2 sofic：一个来自希伯来语的词

1999年，俄裔数学家 Mikhail Gromov（阿贝尔奖得主，这个奖常被称作"数学界的诺贝尔奖"）提出了 sofic 群的概念。Sofic 这个词来自希伯来语里表示"有限"的词根。

用白话讲，一个群是 sofic 的，意思是：你随便截取它乘法表的一小块（任意有限的一块），都能用某个有限集合上的置换把这一块几乎完美地模拟出来。

"置换"就是把一堆东西重新排列。比如把5张牌打乱顺序，就是一个置换。有限集合上的置换是数学里最"老实"、最好算的一类对象。

我自己理解这个概念的时候，用的是这么一个类比：把无限群想象成一个无限精细的三维模型，sofic 就是在问——这个模型能不能用有限多的像素点（体素）无损地渲染出来？如果你把镜头对准任何一小块局部，都能找到一个有限的像素方案完美还原它，那它就是 sofic 的。

那么问题来了：是不是所有可数群都是 sofic 的？

Gromov 提出这个概念之后，这个问题就一直挂在那里。27年，没有人构造出反例，也没有人证明所有群都 sofic。

4.3 为什么这个问题这么要紧

一开始我也以为这只是群论里一个偏门的技术问题。查了一圈之后发现不是。

sofic 性质是一大片理论的地基。 过去二十多年里，数学家在假设"某个群是 sofic"的前提下，建立了一整套理论：

• sofic 熵理论：动力系统里衡量"混乱程度"的核心工具，很多结果的成立前提就是群 sofic；
• 遍历论：sofic 群上的作用有一套专门的理论体系；
• 算子代数：与 Connes 嵌入问题等一系列基础问题纠缠在一起；
• 还有一批著名猜想（比如 Gottschalk 环绕猜想、Kaplansky 直接有限性猜想的若干情形），已经对 sofic 群被证明了。

也就是说，如果"所有群都是 sofic"成立，那这些理论的适用范围就是全部；如果不成立，那就存在某些群，它们根本无法被有限结构逼近，上面这一整片理论的边界要重新划一遍。

这就是为什么加州理工的一位数学博士看到这项结果之后说这是"菲尔兹奖级别的成果"。这个说法本身不是官方评价，属于个人观感，但能反映圈内的第一反应强度。

4.4 Astra 走的是哪条路

这一项的技术路径，官方摘要给的是一句话：论证使用了性质(T)扩张图和二元 Leavitt 代数。

我把这两个词各拆一下。

性质(T)（Kazhdan's property T），是群论里一个"刚性"标签。带这个标签的群非常"硬"——你很难对它做连续形变，它的表示论行为极其受限。直观上可以理解成：这类群拒绝被轻微地扰动。这个"硬"的特性，恰恰是构造反例时需要的——你要证明某个东西不可能被有限置换逼近，就需要它足够硬，硬到任何逼近尝试都会撞墙。

扩张图（expander graph），是图论和理论计算机科学里的核心对象。它是一类"稀疏但连通性极强"的图：边很少，但你怎么切都切不开，任何一小块的邻居都特别多。扩张图在编码理论、随机算法、密码学里到处都是。性质(T)群是构造扩张图的经典来源之一。

二元 Leavitt 代数，是算子代数里一个已经存在的、相当具体的结构。它的关键特征是有一种"自我复制"式的对称性——它可以被拆成两份，每一份都和整体同构。这种自相似性在有限逼近的视角下是个麻烦：有限集合的大小是固定的，没法既是自己又是自己的两倍。

Astra 做的事情，本质上是把这三样东西拼在一起，逼出一个逻辑矛盾。 它从已有的数学工具箱里拎出二元 Leavitt 代数对应的群结构，然后借助性质(T)扩张图的刚性，证明：如果这个群是 sofic 的，就会推出一个不可能成立的结论。所以它不是 sofic 的。

这个思路最让人印象深刻的地方在于——它用的全是现成的工具。二元 Leavitt 代数存在很久了，性质(T)扩张图也不是新东西。27年里无数人在找反例，找的方向大概率是"造一个全新的、奇形怪状的群"。而 Astra 的做法更像是指着工具箱里已经躺了很久的一个物件说：就是它，我证给你看。

我打个粗糙的比方：人类一直在满世界寻找一种"无法被像素化的物质"，四处采集新样本；AI 直接指着桌上那个早就摆着的高维魔方说，别找了。

4.5 谁读过这份证明

这一点我觉得比结论本身更值得写。

官方手稿的各章致谢里，点名了一批真人数学家作为审读者。非sofic群这一章列出的名字包括 Henry Bradford、Michael Chapman、Alon Dogon、Francesco Fournier-Facio 等人——都是群论和算子代数方向的在职研究者。

关键在于措辞：他们是"批判性读者"，不是"共同作者"。这个区分在署名争议里分量很重。OpenAI 的立场很明确：数学论证由系统生成，人类负责准备手稿、完成形式化、并对最终正确性承担责任；把AI完整生成的证明署人类作者，会同时误述系统的贡献和人类智力工作的性质。

这个立场是不是所有人都认同，第十章会展开。但至少在信息披露的完整度上，这次做得比5月那次好得多。

4.6 一个提醒

最后放一句冷水，这也是辛梓煜在词元二号站写技术分析时的一贯习惯——结论再漂亮，也要留出审读窗口。

非sofic群这项结果，形式化证书能保证 Lean 检查过的那条推理链没有漏洞。但它保证不了一件事：被形式化的那个"非sofic群"定义，是不是和群论共同体27年来心里想的那个定义完全一致。定义里悄悄多一个有限性假设、量词位置换一下、假设强一点，形式化系统照样开心地验证通过，但命题的分量就变了。

这不是在暗示这次有问题。这是形式化数学一个已知的软肋，而且是所有形式化项目历史上出岔子最多的地方。第八章我会专门讲这件事。

五、拆解二：高维球堆积——被冻了48年的指数，动了

5.1 从"箱子里塞橘子"讲起

球堆积问题的原始形态特别接地气：给你一个箱子和一堆一样大的橘子，怎么摆能塞进去最多？

三维空间里这个问题就是开普勒猜想。开普勒1611年提出，猜测最密的摆法就是水果摊上那种一层层错位堆叠的方式，密度约74%。这个猜想拖到1998年才被 Thomas Hales 用计算机辅助证明，2014年完成形式化验证。三百多年。

到了高维，问题的性质完全变了。

高维空间的几何直觉是会骗人的。举个经典例子：在高维立方体里，绝大部分体积集中在角落附近，中间那个内接球占的比例小到可以忽略。维数越高，球越"瘦"，空隙越多。所以高维球堆积的密度是指数级衰减的——维数每加一，能塞的比例就掉一大截。

数学家关心的不是某个具体维数下能塞多少，而是这个衰减有多快。

5.2 记号先立起来

记 (\Delta_d) 为 (d) 维欧氏空间里同样大小的球的最大堆积密度。已知的结论是它按指数衰减，形式是：

[\Delta_d \le 2^{-(\alpha+o(1))d}]

这里的 (\alpha) 就是所谓的堆积指数。(\alpha) 越大，说明上界越紧，我们对"最多能塞多少"的认识越精确。

推进 (\alpha)，就是这个方向上最硬的活。

5.3 三个时间锚点

1978年：Kabatiansky 和 Levenshtein。 两位苏联数学家用球面码的方法给出了一个上界，对应的指数是

[\alpha_{KL} = 0.59905576\ldots]

这个数字在此后48年里是所有足够高维度下的最佳一般上界。

2003年：Cohn 和 Elkies。 他们提出了一个完全不同的路子——不绕道球面码，直接用傅里叶分析构造一个线性规划。具体说，考虑函数类

[\mathcal{A}_d=\left{f\in\mathcal{S}(\mathbb{R}^d;\mathbb{R}):\ \hat f(0)>0,\ \hat f\ge 0,\ f\le 0 \text{ 在 } |x|\ge 1 \text{ 上}\right}]

然后定义

[LP_d=\frac{v_d}{2^d}\inf_{f\in\mathcal{A}_d}\frac{f(0)}{\hat f(0)}]

其中 (v_d) 是单位球体积。任何满足这些条件的辅助函数 (f) 都会给出一个密度上界，于是 (\Delta_d\le LP_d)。

这个方法在低维威力惊人。2016到2017年，Maryna Viazovska 用它解决了8维的球堆积问题，随后与 Cohn、Kumar、Miller、Radchenko 合作解决了24维。她因此在2022年拿到菲尔兹奖。

但高维行为一直是个谜。 Cohn 和 Zhao 在2014年证明了 Cohn–Elkies 线性规划至少和 Kabatiansky–Levenshtein 界一样强，但它到底能不能严格改进那个经典指数，没人知道。2020年 Afkhami-Jeddi、Cohn、Hartman、de Laat、Tajdini 一群人（受共形场论里"模自举"方法的启发）猜了一个具体的高维速率，但只是猜想。

2026年：Astra 把这个猜想证了。

5.4 结果本身

手稿第1章的主定理是：

[\lim_{d\to\infty} LP_d^{1/d}=\sqrt{\frac{e}{2\pi}}]

也就是说，Cohn–Elkies 线性规划的精确渐近强度被确定了。换算成指数形式：

[\Delta_d\le LP_d = 2^{-(\alpha^+o(1))d},\qquad \alpha^=\tfrac{1}{2}\log_2\frac{2\pi}{e}=0.6044\ldots]

对比一下：

差值看起来只有0.005，但这是指数上的0.005。在1000维下，这意味着上界收紧了大约 (2^{-5}) 倍；维数越高，差距越大。更重要的是心理意义：这个数字48年没动过。

5.5 还有一个配套结论

主定理还顺带解决了另一个问题：傅里叶符号不确定性问题的渐近形式。

这个问题问的是：如果一个函数 (g) 是自己傅里叶变换的特征函数（(\hat g=\pm g)），并且在原点取值为0，那么它最早从哪个半径开始就一直非负？记这个临界半径的最优值为 (A_\pm(d))。手稿证明了：

[\lim_{d\to\infty}\frac{A_+(d)}{\sqrt d}=\lim_{d\to\infty}\frac{A_-(d)}{\sqrt d}=\frac{1}{\pi}]

两个常数的渐近值都是 (1/\pi)。这个 (1/\pi) 通过 Stirling 公式换算，恰好就给出了 (\sqrt{e/2\pi}) 那个堆积指数。附录里还额外证明了一个精细结论：对每个维数 (d\ge 1)，严格有 (A_+(d)<A_-(d))。

顺便说一句，这个符号不确定性问题在物理里也有影子——它出现在无自旋模自举里，模S反对称性会产生反自傅里叶的测试函数，其最终符号控制着谱隙。所以这不是一个纯粹自娱自乐的技术问题。

5.6 一个关键的"封顶"结论

主定理里有一句话，很容易读漏，但分量极重：

匹配的下界表明，没有任何 Cohn–Elkies 辅助函数能够改进这个指数。

翻译一下：(0.6044\ldots) 不只是"目前最好的"，而是这条技术路线的天花板。你再怎么精心构造辅助函数，都不可能超过它。想继续往前推，必须换一套完全不同的方法。

这个结论的价值不亚于改进本身。它等于给整个领域画了一条线：这个方向已经走到头了，别在这里继续挖。对一个领域来说，知道哪条路走到尽头，和知道哪条路能往前走，同等重要。

5.7 第2项：编码理论那边同时也破了

第2章处理的是相关但独立的问题：码的最大规模。

二进制码是一堆0/1串，要求任意两个串之间至少差 (d) 位（这样传输出错时才能纠回来）。给定相对距离 (\delta)，问最多能有多少个码字？经典的最佳一般界是1977年 McEliece、Rodemich、Rumsey、Welch 给出的（业内叫 MRRW 界）。球面码那边对应的是1978年 Kabatiansky–Levenshtein 界。

手稿第2章的结论是：这两个经典指数都被严格改进了，而且是对所有参数范围。原文措辞是"这是自1977年和1978年以来对各自一般高维指数的首次改进"。

技术上，它构造了一类新的"两点线性规划证书"。经典构造里，每个保留的调和空间只贡献一个与码点关联的向量；新构造给每个码点关联一个指数级大的子空间，子空间随着码点一起移动。这个"把一条线换成一个大空间"的想法，是整章的核心。

而且第2章在 (s\to 1) 的极限下，独立地重新导出了第1章的球堆积指数。两条路走到同一个答案——这种自洽性在数学里是很强的可信度信号。

六、拆解三：Connes 刚性猜想，被无限多个反例埋了

6.1 冯·诺依曼代数是什么

先建立最基础的直觉。

给定一个群 (G)，你可以按一套标准手续，从它造出一个叫做群冯·诺依曼代数的东西，记作 (L(G))。这个过程会丢掉一些信息——就像把一个立体物件投影到平面上，投影里保留了一部分特征，也丢掉了一部分。

自然的问题是：这个投影丢了多少？能不能从投影反推出原来的群？

1982年的菲尔兹奖得主、非交换几何的奠基人 Alain Connes 提出了一个猜想，方向是"丢得不多"。具体地说，对于某一类特殊的群——带**性质(T)**标签的那些——他猜测 (L(G)) 能唯一确定 (G)。

用一个比喻：Connes 猜测，对这类群而言，冯·诺依曼代数就像指纹一样独一无二。你看到指纹，就知道是谁。

6.2 为什么是性质(T)群

这里的选择不是随便的。第四章讲过，性质(T)是一个"刚性"标签，带这个标签的群非常硬，很难形变。

直觉上，越硬的东西，投影里保留的信息应该越多。所以如果唯一确定性在哪一类群上成立，最有希望的就是性质(T)群。Connes 的猜想赌的就是这个直觉。

几十年里，这个猜想的两个方向都没有决定性进展。数学家在这个迷宫里绕了很久。

6.3 Astra 给出的答案：不成立，而且远不成立

手稿第4章的结论是：

构造出无限多个两两不同构的性质(T)群，它们拥有完全相同的群冯·诺依曼代数。

拆开看这句话：

• 无限多个——不是找到一对反例交差；
• 两两不同构——这些群彼此长得完全不一样，不存在任何群同构把其中一个变成另一个；
• 相同的冯·诺依曼代数——但它们的投影，一模一样。

这不是"猜想有个例外"，这是"唯一性彻底崩了"。

还有一个附带结论：这个构造同时回答了 Sorin Popa 提出的一个相关的"有限对一"问题。Popa 是算子代数领域最重要的研究者之一，而且——他本人是这一章的审读者之一，名字出现在致谢里。手稿这一章的致谢还包括 François Charles。

我觉得这个安排挺有说服力的：提出相关问题的人，亲自读了推翻它的证明。

6.4 打个比方

Connes 的猜想相当于断言"世上没有两片雪花拥有完全相同的内部原子结构"。

Astra 不仅找到了两片一模一样的，它直接下了一场暴风雪——无限多片雪花，外观各不相同，但核心的代数结构完全相等。

这个比方是我自己想的，不算严谨，但抓住了要点：反例的强度，不在于"存在"，而在于"批量存在"。

6.5 这一项为什么被单独拎出来评价

按 Epoch AI 的 OpenMath 评分体系，一些评估把这十项里的大部分归为"重大进步"（Major Advance），而其中有个别项被单独评为"突破"（Breakthrough）级别——具备走出专业圈层、成为全年数学领域最佳成果候选的潜质。

需要说明的是，这类评分本身带有相当大的主观性，而且是在同行系统审读之前给出的。我建议把它当成一个"圈内第一反应的温度计"，而不是最终定论。

真正的定论，要等这些结果被写进论文、投出去、被审稿人逐行看过、被后续工作引用和推广之后才会有。那通常需要一到两年。

6.6 这三项的共同点

回过头看第四、五、六章讲的这三项，我发现它们有个共同点，而且这个共同点比结论本身更有信息量：

它们都不是靠"算力硬怼"出来的。

球堆积那一项的核心是一个 Mellin 变换上的技巧——通过在对数半径坐标下做 Poisson 外推，把符号条件转化成一个质量估计，再用 Stirling 公式换算成指数。这是一条需要"想到"的路，不是一条可以枚举出来的路。

非sofic群那一项的核心是把三样现成工具拼在一起产生矛盾。拼法是关键，工具都是公开的。

Connes 那一项的核心是找到一个能批量生产"外观不同、投影相同"的群的构造机制。

这三件事，都属于"你得先有一个想法"的范畴。这就是为什么 OpenAI 那边的研究者说，测试时计算远未封顶——他们相信这种"想法"是可以通过更多推理算力堆出来的。同一批人也承认，他们尝试过其他难题，目前还没有拿下任何一个类似黎曼猜想那样的千禧年大奖级问题。

这两句话要放在一起读，才不会失真。

七、其余七项速览：从算术电路到拉姆齐数

前面三项讲得细，剩下七项我用相对紧凑的方式过一遍。每一项都按"问题是什么—结果是什么—为什么重要"三段来写。

7.1 算术电路复杂度：permanent 的下界

问题是什么。 矩阵有两个长得很像的量：行列式（determinant）和积和式（permanent）。它们的定义几乎一样，唯一区别是行列式里有个正负号交替，permanent 里全是加号：

[\mathrm{perm}(A)=\sum_{\sigma\in S_n}\prod_{i=1}^{n}a_{i,\sigma(i)}]

就差这一个符号，计算难度天差地别。行列式有高斯消元，多项式时间搞定；permanent 被证明是 #P-完全的，一般认为没有高效算法。

"计算 permanent 到底需要多大的电路"，是复杂性理论最核心的问题之一。它和 VP vs VNP（代数版本的 P vs NP）直接相关。

结果是什么。 Astra 给出了两个新下界：

• 无除法电路（division-free circuits）计算 permanent，需要 (\Omega(n^2\log\log n)) 个门；
• 算术公式（formulas）计算 permanent，需要 (\Omega(n^4/\log n)) 个叶节点。

为什么重要。 电路下界是复杂性理论里出了名的难。证明"某个函数需要很大的电路"，几十年来进展极其缓慢，甚至有一整套"自然证明障碍"理论在解释为什么这么难。任何一点推进都是硬通货。

7.2 量子平行重复定理

问题是什么。 经典复杂性理论里有一条基础原理：把一个博弈同时玩很多轮，作弊者通过全部检验的概率会指数级下降。这个原理叫平行重复定理，是 PCP 理论和不可近似性证明的基石。

推广到量子情形一直很难。因为量子玩家可以共享纠缠——多轮之间可能存在经典情形下不存在的关联，让"独立性"这个前提失效。此前只对一些特殊类别的量子博弈有结果。

结果是什么。 对每一个有限的两人纠缠博弈，证明了指数级平行重复。不再限于特例。

为什么重要。 这条定理是量子复杂性理论里长期缺失的一块地基。补上之后，一整批依赖它的结果可以往前推。

7.3 最近向量问题（CVP）的近似难度

问题是什么。 给你一个格（lattice，可以想成高维空间里规则排布的点阵）和一个目标点，找到离目标点最近的格点。这就是 CVP。

它是格理论的基础问题，也和后量子密码学直接相关——目前主流的抗量子加密方案，安全性基础就建立在格问题的困难性上。

结果是什么。 通过从 3SAT 的直接归约，证明了欧氏 CVP 存在 (n^{1/400}) 因子的近似难度。同时对二进制译码和其他格范数下的问题给出了相关推论。

为什么重要。 "直接归约"这三个字是重点。此前的难度结果往往要绕好几道弯，而直接归约给出的结构更干净，也更容易推广。这类结果对评估后量子密码方案的安全边界有直接参考价值。

7.4 Ehrhart 体积猜想

问题是什么。 考虑一个凸体，要求它的重心是它内部唯一的格点（也就是说，除了重心，内部再没有整数坐标的点）。这样的凸体，体积最大能到多少？

结果是什么。 在每个维度上都证明了紧界：

[V_{\max}=\frac{(n+1)^n}{n!}]

为什么重要。 这是一个几十年的老猜想，而且答案是一个极其干净的闭式。数学里，"猜想成立且界是紧的"这种结论并不多见——大多数情况下你只能证明一个不那么紧的界。这个结果在所有维度上一次性给全了。

顺便一提，((n+1)^n/n!) 这个表达式在 (n) 大时约等于 (e^n/\sqrt{2\pi n})，增长速度接近 (e^n)。

7.5 多色拉姆齐数：埃尔德什第183号问题

问题是什么。 拉姆齐理论研究的是"足够大的混乱里必然出现秩序"。最经典的版本：一场聚会里至少要有多少人，才能保证要么有3个人互相认识，要么有3个人互相不认识？答案是6。

多色版本是：用 (k) 种颜色给完全图的边染色，至少要多少个顶点，才能保证一定存在一个单色三角形？这个最小顶点数记作 (R_k(3))。

这个量的上下界之间一直有个大缺口。埃尔德什把它列为自己问题库的第183号。

结果是什么。 给出了超指数下界，确定了

[R_k(3)=k^{\Theta(k)}]

为什么重要。 (k^{\Theta(k)}) 是一个精确到指数阶的刻画，把长期存在的缺口合上了。而且埃尔德什问题库有明确编号和状态记录，这一条的"是否真的开放"没有任何争议空间。

7.6 紧致性与退化性猜想：一次干掉两个

问题是什么。 极值图论研究的是"图里边最多能有多少而不出现某种子结构"。这里涉及两个猜想：

• 紧致性猜想（Erdős–Simonovits，埃尔德什问题库第146号）；
• 退化性猜想（Erdős，第180号）。

两者都关于所谓 Turán 型问题的结构性质。

结果是什么。 用两组独立的二部图构造，分别把这两个猜想证伪了。

为什么重要。 一次公告解决三个埃尔德什问题（加上7.5的183号），这在组合数学里是相当罕见的密度。埃尔德什生前提出了上千个问题，很多至今悬着，每解决一个都会被记录在案。

7.7 把这七项串起来看

我列个小表收尾：

有件事我一开始没注意，后来越想越有意思：这七项分布在完全不同的子领域，用的工具几乎没有重叠。电路下界要的是代数复杂性那一套，量子平行重复要的是算子和信息论工具，Ehrhart 要的是凸几何和格点计数，拉姆齐数要的是概率方法和构造。

一个数学家能在其中两三个方向上同时做出研究级贡献，已经很少见了。全部七个方向同时来一遍，这才是这份手稿真正让人坐直的地方——不是单点深度，而是横跨的广度。

八、方法论：Lean 4 验的是什么，不验什么

这一章是全文最有实操价值的部分。看懂它，你以后遇到任何"AI证明了某某"的新闻，都能自己判断分量。

8.1 形式化验证是什么

先讲最基础的。

平时数学论文里的证明，是用自然语言（加上一堆符号）写的。审稿人读一遍，判断每一步是否成立。这个过程依赖人的理解和经验，而人会看漏。数学史上出过不少"发表多年后才发现有洞"的案例。

形式化验证换了一条路：把证明的每一步都写成一种严格的、机器能解析的语言，然后让计算机逐步检查每一步是否严格遵循了逻辑规则和已有定理。计算机不理解"直觉上显然"，它只认规则。

Lean 4 就是这类工具里目前最活跃的一个。它背后有 mathlib——一个由全球志愿者维护的形式化数学库，已经把从集合论、代数、拓扑到分析的大量基础内容形式化进去了。

一个最简单的 Lean 4 片段大概长这样：

-- 证明：任意自然数 n，n + 0 = n
theorem add_zero_example (n : Nat) : n + 0 = n := by
  simp

-- 证明：加法交换律的一个实例
theorem add_comm_example (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b

真实的研究级证明当然复杂得多，可能是几千行甚至上万行。但原理一样：每一步都必须能被机器验证，没有"这里显然成立"的余地。

8.2 这次的完整流程

官方披露的流程是这样的，我画成流程图：

flowchart LR
    A[开放问题输入] --> B[Astra 生成数学论证]
    B --> C[人类研究者 + 同一模型<br/>整理成手稿]
    C --> D[模型将论证形式化为 Lean 4]
    D --> E[Lean 编译器逐步核验]
    E --> F{通过?}
    F -->|是| G[生成机器可检验证书<br/>开源发布]
    F -->|否| B
    G --> H[数学家批判性审