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

• Read the paper
• Read the reasoning walkthroughs

The results

1. High-dimensional sphere packing: Improved asymptotic upper bounds on sphere-packing density, reaching the Cohn–Elkies threshold. (SpherePacking.lean)
2. Binary and spherical codes: Exponentially stronger upper bounds for binary codes at every minimum distance, together with corresponding bounds for spherical codes. (MetricCodes.lean)
3. Non-sofic groups: A construction of a non-sofic group, resolving whether every group admits finite permutation approximations. (NonSoficGroup.lean)
4. Connes’s rigidity conjecture: A counterexample to the conjecture that certain groups are determined by their group von Neumann algebras. (ConnesRigidity.lean)
5. Arithmetic circuit complexity: New lower bounds for computing the permanent with arithmetic circuits and formulas, including an