せいぜい分かるのは、「数学者によって証明されている定理」の
ほとんどは「形式的にも証明できる」だろう、という予想でしょ。

よく考えたらゲーデルの第二不完全性定理があるじゃん。

「無矛盾性を意味する（とある）命題」が正しいけれども、
それは形式体系では証明できないって定理だね。