Normality of mathematical constants

Despite extensive empirical evidence—billions of digits have been computed for $\pi$, $e$, and $\sqrt{2}$, all showing near-uniform digit distribution—it is an open problem whether any of the classical constants $\pi$, $e$, $\sqrt{2}$, $\ln 2$, or $\varphi$ is normal in any base.

References:

• Wikipedia (Normal number)
• Wikipedia (Pi)

theorem NormalNumber.pi_normal_base_ten : IsNormalInBase 10 Real.pi

$\pi$ is normal in base 10.