Prove BinarySweep (openai/math family 238: Optimal logarithmic mixing of the Thorp shuffle) in Lean 4 with…
Prove BinarySweep (openai/math family 238: Optimal logarithmic mixing of the Thorp shuffle) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 238 of the release, Optimal logarithmic mixing of the Thorp shuffle (Probability and…
The task
Context: this statement belongs to family 238 of the release, *Optimal logarithmic mixing of the Thorp shuffle* (Probability and statistical mechanics). The family as a whole: Proves that the Thorp shuffle randomizes $N=2^d$ labeled cards in $\Theta(\log N)$ physical shuffles, settling its optimal mixing order for…
Part of raising-heart/openai-math.