openai/ten-proofs

# 数学与理论计算机科学领域的十项进展 本仓库包含以下成果的 Lean 4 形式化： OpenAI 的 [数学与理论计算机科学领域的十项进展](https://openai.com/index/ten-advances-in-mathematics/)。 - [阅读论文](https://cdn.openai.com/pdf/ten-proofs-oai.pdf) - [阅读推理过程详解](https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf) ## 研究成果 1. **高维球体填充：** 改进了球体填充密度的渐近上界，达到了 Cohn–Elkies 阈值。 ([`SpherePacking.lean`](SpherePacking.lean)) 2. **二元码与球面码：** 针对任意最小距离的二元码，得到了指数级增强的上界，并为球面码推导出了相应的界限。 ([`MetricCodes.lean`](MetricCodes.lean)) 3. **非 sofic 群：** 构造了一个非 sofic 群，从而解决了是否所有群都存在有限置换近似的问题。 ([`NonSoficGroup.lean`](NonSoficGroup.lean)) 4. **Connes 刚性猜想：** 给出了该猜想的反例，该猜想认为某些群可由其群 von Neumann 代数唯一确定。 ([`ConnesRigidity.lean`](ConnesRigidity.lean)) 5. **算术电路复杂性：** 在使用算术电路和公式计算积和式方面得出了新的下界，包括 $n^4 / \log n$ 的公式下界。 ([`Permanent.lean`](Permanent.lean)) 6. **量子并行重复：** 针对任意有限的两人量子博弈，证明了指数级并行重复定理。 ([`QuantumParallelRepetition.lean`](QuantumParallelRepetition.lean)) 7. **最近向量问题：** 证明了最近向量问题在多项式因子下的近似硬度，并为解码和格问题带来了相关推论。 ([`GapCVP.lean`](GapCVP.lean)) 8. **Ehrhart 体积猜想：** 确定了在每个维度下，其几何中心是唯一内部格点的凸体的最大锐利体积。 ([`EhrhartVolumeInequality.lean`](EhrhartVolumeInequality.lean)) 9. **多色 Ramsey 数：** 给出了多色三角形 Ramsey 数的超指数级下界，解决了 Erdős 问题 183。 ([`MulticolorTriangleRamsey.lean`](MulticolorTriangleRamsey.lean)) 10. **极值数猜想：** 给出了极值图论中紧致性与退化性猜想的反例，解决了 Erdős 问题 146 和 180。 ([`CompactnessAndDegeneracy.lean`](CompactnessAndDegeneracy.lean)) ## 构建形式化 本项目使用 Lean 4.32.0、mathlib 和 Lake。在安装 [elan](https://github.com/leanprover/elan) 之后，获取 mathlib 缓存 并构建所有十个形式化，请使用以下命令： ``` lake exe cache get lake build All ``` 要构建单个形式化，请将其模块名称传递给 Lake： ``` lake build SpherePacking ``` ## 独立证明检查 有关使用 Comparator 检查形式化的说明，请参阅 [ComparatorChallenges README](ComparatorChallenges/README.md)。

标签：Lean, 定理证明, 形式化验证, 数学, 理论计算机科学