为什么值得关注

它将多项近期重大进展（其中一些解决了长期猜想）转化为可由机器检查的 Lean 证明，让形式化验证社区更容易接触这些成果。

适合谁使用

对形式化证明验证感兴趣的数学家
从事复杂度、编码和量子博弈研究的理论计算机科学家
Lean/mathlib 用户及形式化证明开发者
数学或计算机科学专业的研究生

典型使用场景

验证或探索重要定理的机器检查证明
在新的 Lean 项目中复用这些形式化引理和构造
学习如何在 Lean 中编码高级数学与理论计算机科学结果
在大型多样化形式化项目上检验证明助手的能力

项目优势

在单一仓库中涵盖了数学与理论计算机科学领域的十个不同高级结果
模块化结构：每个结果有独立 Lean 文件，可通过 Lake 单独构建
使用 Lean 4.32.0、mathlib 和缓存命令，搭建环境可复现
提供使用 Comparator 进行独立证明检查的说明

使用前须知

需要 Lean 生态（elan、Lake、mathlib）且最好熟悉 Lean 工具链才能构建或检查
README 仅列举结果，未提供详细数学解释或教程
形式化代码绑定 Lean 4.32.0，未来版本或库变动可能需要进行适配

README 快速开始

Ten Advances in Mathematics and Theoretical Computer Science

This repository contains Lean 4 formalizations of the results presented in Ten advances in mathematics and theoretical computer science by OpenAI.

The results

High-dimensional sphere packing: Improved asymptotic upper bounds on sphere-packing density, reaching the Cohn–Elkies threshold. (SpherePacking.lean)
Binary and spherical codes: Exponentially stronger upper bounds for binary codes at every minimum distance, together with corresponding bounds for spherical codes. (MetricCodes.lean)
Non-sofic groups: A construction of a non-sofic group, resolving whether every group admits finite permutation approximations. (NonSoficGroup.lean)
Connes’s rigidity conjecture: A counterexample to the conjecture that certain groups are determined by their group von Neumann algebras. (ConnesRigidity.lean, ConnesRigidity/)
Arithmetic circuit complexity: New lower bounds for computing the permanent with arithmetic circuits and formulas, including an $n^4 / \log n$ formula lower bound. (Permanent.lean)
Quantum parallel repetition: Exponential parallel repetition for arbitrary finite, two-player quantum games. (QuantumParallelRepetition.lean)
Closest vector problem: Polynomial-factor hardness of approximation for the closest vector problem, with related consequences for decoding and lattice problems. (GapCVP.lean)
Ehrhart’s volume conjecture: The sharp maximum volume in every dimension for a convex body whose centroid is its only interior lattice point. (EhrhartVolumeInequality.lean)
Multicolor Ramsey numbers: A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183. (MulticolorTriangleRamsey.lean)
Extremal number conjectures: Counterexamples to the compactness and degenerac

项目描述

Lean certificates accompanying proofs in mathematics and theoretical computer science

ten-proofs