高维空间中最多能塞进多少球？
球体堆积（sphere packing）是几何数论与编码理论共同的核心问题：在 n 维空间中放置互不重叠的等大球体，最多能占据多大体积比例？
密度上界的每一次推进都牵动编码与格论：一个球体堆积对应一族离散的格点，而格的“好”程度直接决定纠错码的容量。三维的开普勒猜想由 Hales 于 1998 年证明，E₈ 格与 24 维 Leech 格的最优性则于 2016 年由 Viazovska 等人借助 Cohn–Elkies 线性规划方法完成。
但对于一般维数，指数级上界自 1978 年前后由 Rogers 等人建立以来几乎停滞——学界一直没有找到能在任意维统一改进的工具。
指数推进到 Cohn–Elkies 阈值
Astra 给出新的球体堆积密度上界，将指数推进到 Cohn–Elkies 线性规划阈值。这是四十多年来一般维数球体堆积指数上界的首次系统性改进，意味着此前被普遍接受的“指数壁垒”被打破。
该结果并不依赖构造更优的格，而是对密度上界的分析工具本身做出了实质性推进，方法与 Cohn–Elkies 的 Fourier 方法直接衔接。
- 首次在一般维数统一改进球体堆积指数上界
- 与 2016 年 Viazovska 的 E₈ / 24 维最优性证明同源于线性规划框架
- 同时为上界与下界的长期缺口研究提供了新坐标
据 OpenAI 公开资料，这是自 1978 年以来一般球体堆积指数的首次改进。
高维结构的“容量天花板”被重新标定
球体堆积上界与纠错码、数据编码和高维近似计算紧密相关。上界越紧，说明高维空间中规则结构的极限越清晰，这直接影响编码理论中关于最大码规模的认知。
多位数学家认为，这一结果与编码理论领域的二元码与球面码突破形成互补，共同勾勒出高维离散结构研究的新图景。
从论证到可复核的证明
OpenAI 将本成果的论证整理进 249 页论文，并转化为 Lean 4 形式化证明文件，主要定理的 sorry_count 为 0，仅使用三类标准公理。
研究者可在本地重跑证明文件，逐行核对推理步骤，而非依赖对“AI 结论”的信任。
深入阅读
本页内容主要整理自以下公开资料。成果仍需数学共同体长期审查，欢迎据此追踪原始文献与 Lean 证明文件。
- OpenAI 官方发布OpenAI 于 2026-08-01 公布 Astra 十项数学与理论计算机科学进展。
- 249 页论文与 Lean 证明文件论文、62 页解题思路说明与 Lean 4 形式化证明证书已在 GitHub 开源，可本地复现。
本课题来自 OpenAI Astra 于 2026-08-01 公布的十项数学与理论计算机科学突破，编号 №01。想参与验证或深入研究，可加入 NiuMaAgent 社区 Fork 对应研究仓库。
加入 牛马智能体，开启你的开源科研之路
NiuMaAgent 以 Apache License 2.0 开源协议发布。欢迎 Fork、提交 Issue， 与全球科研人员共建 AI4Science 生态。