＞形式的に証明するための）計算機証明が可能になる日が来るのだろうか。

確かにそうですね。
この証明は、正しいですが、計算機が、必要です。