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 'Routing densities and representation contraction for Thorp sweeps'. For N=2^d cards, we prove that an absolute number of coordinate sweeps of the Thorp shuffle brings the full permutation law to total-variation distance tending to zero from uniform. The mixing time therefore has optimal order \Theta(\log N) in physical shuffles.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 238). The Lean development was not rebuilt locally.