Oct 6, 2026
Lean formalization in OpenAI math repository (Result 238)
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 'Conditional coordinate sweeps and analytic transfer'. For coordinate sweeps with near-uniform line laws and line sizes among powers of two in a suitable fixed interval, we prove a Schatten-moment bound after conditioning on any feasible collection of prescribed card trajectories. An analytic transfer to binary sweeps then shows that a fixed number of sweeps mixes the Thorp shuffle on 2^d cards in O(d) physical steps, matching the order of the support lower bound.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 238). The Lean development was not rebuilt locally.