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 'Compatibility entropy and the spectrum of a Thorp sweep'. We prove that the Thorp shuffle on n=2^d cards mixes in \Theta(d) physical shuffles. After a sufficiently large fixed number of coordinate sweeps, the total-variation distance of the full permutation from uniform tends to zero as d\to\infty.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 238). The Lean development was not rebuilt locally.