Oct 6, 2026
Lean formalization in OpenAI math repository (Result 092)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A single-lattice covering bound of order n log n'. Every convex body in ℝn, n ≥ 2, admits a covering by translates along one full-rank lattice with density at most Cn\log n, for an absolute constant C. No symmetry or boundary regularity is assumed.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 092). The Lean development was not rebuilt locally.