Blueprint

This repository contains a refactored version of OpenAI's formalization of their results on the Cohn–Elkies linear programming bound for sphere packings and Bourgain-Clozel-Kahane's sign uncertainty principle for Fourier eigenfunctions. One-file version can be found in SpherePackingRefactored.lean, which is about 58% of the original SpherePacking.lean (55,616 lines) in terms of LoC while containing several additional results. More organized formalization are under CohnElkies and CohnElkiesForMathlib, with a blueprint of the statements and proofs in CohnElkiesBlueprint.

Some results in the original report were missing in their formalization, and we have added them here. In particular, we have formalized both signs of the uncertainty principle, the self-Fourier function $f_0$, $L^1$ to Schwartz reduction, radial reduction. and Proposition A.1 ($A_+(d) < A_-(d)$ for all $d \ge 1$). Also, the proof of Lemma 3.2, whose original formal proof uses the Phragmén–Lindelöf principle on a strip, is replaced by a proof using Poisson inequality for subharmonic functions (following the informal proof). The Phragmén–Lindelöf principle based proof is still kept. The 30-digits approximation of the Cohn-Elkies exponent is removed, since it is unnecessary.

Every code is written by Claude (mostly Fable 5.1 and Opus 5), where the details can be found under formalization.yaml. It was asked to follow RefactoringPlan.md (which is completely human-written) with the original OpenAI's report, original Lean file, and my two blog posts as references, and the result is summarized in RefactoringResult.md.

The statements in ComparatorChallenges/CohnElkies.lean are compared with the proofs in the CohnElkies library by

lake exe comparator ComparatorChallenges/CohnElkies.json

with landrun (Linux only), lean4export (built with this project's toolchain: lake build @lean4export/lean4export) and optionally nanoda_bin on PATH; the workflow .github/workflows/comparator.yml runs this in CI. See ComparatorChallenges/README.md.

Apache License 2.0 (see LICENSE and NOTICE). The development started from SpherePacking.lean of openai/ten-proofs (Apache-2.0), which itself reuses material from Sphere-Packing-Lean (Apache-2.0).