I understand that there is currently no proof in any base for whether $\pi$ is normal or disjunctive.
Are there any proofs of whether specific sequences of numbers are infinitely occurring in $\pi$? For instance, is there a formal proof that 1 is infinitely occurring in the decimal expansion of $\pi$?