RANLUXについて考えていた

RANLUX乱数生成法の特徴に、「異なるシードのジェネレータ間では、乱数列が重複しないことが数学的に保証されている」というのがあって、それをどうやって検証しようかと考えていた。

RANLUXは乱数の周期が2の171乗あるから、その長さの数列を1億個くらいのシードのバリエーションで作って比較すれば検証できるけど、1ヶ月くらい計算が終わりそうにない(並列化して、かつメモリ節約のために乱数列を一方向ハッシュ関数でハッシュ化すれば、ある程度改善が見込める)。
なのでこういう場合にはブルートフォース的な総当たりは向いていなくて、Coqのような定理証明系言語を使うのが適切なんだろうなーと思った。