【３】コンピュータが必要とされる証明

　コンピュータが必要とされる有名な証明の例が４色問題とケプラー予想の証明である．１９７６年，アッペルとハーケンは４色問題を証明するのにコンピュータを１０００時間費やして，２０００個の特殊なケースへと還元した．

また，１９９８年，ヘールズの証明したケプラー予想はヒルベルトの有名な２３問題の１８番目となる離散幾何学の最も古い問題である．ヘールズの証明は２５０ページの論文と３ギガバイトのコンピュータプログラムからなるという．

　これらを手作業で１字１句まで確かめるには膨大な時間がかかるため，事実上不可能であって，信用するしかない．とりあえず，信ずる者は救われる，ホレ信じなさいというわけであるが，どうしても天下り式で我慢できない方もいるだろう．４色問題とケプラー予想のコンピュータを使わない証明にはこれまでにないようなまったく新しいアイディアが必要になると思われるが，そうしたアイディアは今日もなお登場していない．いまのところ，４色問題とケプラー予想の証明を検証するには検証用のコンピュータソフトを作るしかないものと思われるが，それとてたいそう時間の要る取り組みとなるだろう．

＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝＝