＞今度は計算機とそのプログラムの信頼性の問題が出てくるわけで
＞往々にして健全な直観の方が信頼が置けたりするわけで
それは今のところね。しかも、健全な直観を獲得するのは
ごく専門領域に限ったとしても大きな労力を要することは
君もよく知っているはずだよね

だから、コンピュータによる自動化が今後なされることは、
それなりに意味のあることだろう。まだ実用段階にはない
だろうけど。特に数学の証明問題の自習に役立つと思うし、
数学者だって自分の証明のチェックに使えるだろう