十大数学与理论计算机科学进展
本仓库包含OpenAI在数学与理论计算机科学十大进展中提出的结果的Lean 4形式化。
结果
- 高维球填充： 改进了球填充密度的渐近上界，达到了Cohn–Elkies阈值。(
SpherePacking.lean) - 二进制码和球形码： 在每个最小距离上为二进制码提供了指数级更强的上界，以及相应的球形码界限。(
MetricCodes.lean) - 非Sofic群： 构造了一个非Sofic群，解决了每个群是否都允许有限置换近似的问题。(
NonSoficGroup.lean) - Connes刚性猜想： 反驳了某些群由其群von Neumann代数决定的猜想。(
ConnesRigidity.lean) - 算术电路复杂性： 计算永久项的算术电路和公式的新下界，包括$n^4 / \log n$公式下界。(
Permanent.lean) - 量子并行重复： 任意有限双人量子游戏的指数级并行重复。(
QuantumParallelRepetition.lean) - 最近向量问题： 最近向量问题的多项式因子近似困难性，以及对解码和格问题的相关后果。(
GapCVP.lean) - Ehrhart体积猜想： 在每个维度上，对于质心是其唯一内部格点的凸体，给出了最大体积的精确值。(
EhrhartVolumeInequality.lean) - 多色Ramsey数： 多色三角形Ramsey数的超指数下界，解决了Erdős问题183。(
MulticolorTriangleRamsey.lean) - 极值数猜想： 极值图论中紧致性和退化性猜想的反例，解决了Erdős问题146和180。(
CompactnessAndDegeneracy.lean)
构建形式化
本项目使用Lean 4.32.0、mathlib和Lake。安装elan后，获取mathlib缓存并构建所有十个形式化：
lake exe cache get
lake build All
要构建单个形式化，将模块名称传递给Lake：
lake build SpherePacking
独立证明检查
有关使用Comparator检查形式化的说明，请参阅ComparatorChallenges README。