擬似乱数を1bit伸ばすことができれば、任意の長さの擬似乱数に伸ばすことができます。この定理をLean4で形式化しました。 定理4.1 擬似乱数生成器$G : \{0,1\}^n \rightarrow \{0,1\}^{n+1}$に対し、$G':\{0,1\}^n \rightarrow\{0,1\}^L$を「 $x_0 = x, i=0,…