Public Lean 4 repository accompanying OpenAI’s “Ten advances in mathematics and theoretical computer science” (Aug 1, 2026). Contains formalizations for sphere packing, metric/binary/spherical codes, arithmetic circuit complexity, non-sofic groups, Connes rigidity, quantum parallel repetition, closest vector problem, Ehrhart volume, multicolor Ramsey, and extremal Erdős problems. Uses Lean 4.32.0, mathlib, Lake. Apache-2.0 license. PDFs for paper and reasoning walkthroughs linked from README.