＞ 四色問題の定理の証明は、本当の意味で読んだ人間はいないと思う。
これは怖い話ですね。森毅の本にも、チューリング賞をとったホアの講演を
聞いたと言う話があるのですが、ホアはエイダという米国防総省が開発した
プログラム言語を原子力やその他の重要な部門では使わないように、と
語ったそうです。
バグがあるからですが、このバグはどこに潜んでいるかわからない。、
自身のプログラムは、精査するでしょうが、OS、言語にある場合、これは一般の人間
の能力では見つけることは不可能です。
CPUのなかに存在したこともあって報じられたことがあります。