Do we know that if $\pi$ is normal then there is a proof of it?

Question

We do not know whether $\pi$ is normal or it is not and many other weaker statements, e.g. (*) $\pi$ contains infinitely many $0$s.

Inspired by the Godel's incompleteness theorem that there are some true statements which cannot be proved, do we currently know that

1) if $\pi$ is normal then there is a proof of it,

2) if $\pi$ is not normal then there is a proof of it?

I suppose that we do not know much in this direction, however is there at least a proof for a much weaker property of $\pi$ of a similar kind to (*)?

References:

Does Pi contain all possible number combinations?

https://mathoverflow.net/questions/51853/what-is-the-state-of-our-ignorance-about-the-normality-of-pi