２００２年と２００３年にロシアの数学者ペレルマンがポアンカレ予想に関する３つの論文をインターネット上に掲載した．それは正しいことが検証され，これでクレイ数学研究所が提示した７つのミレニアム懸賞問題のうちポアンカレ予想は解決，残りは６つとなった．ペレルマンは２００６年にその業績でフィールズ賞を受賞したが，辞退している．

　１９９４年，ワイルズはフェルマーの最終定理を証明した．私はポアンカレ予想の証明がどれくらいの長さになったのか知らないが，フェルマー予想の証明は約２００ページにおよぶそうである．とはいってもこの証明は長さの点ではほんの序の口にすぎない．これまでの記録は有限単純群の分類に関する論文で，１９８０年代に発表された１００以上の論文の証明全体の長さは１万５千ページにもおよぶとされている．

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

　　４ｆ2＋３ｆ3＋２ｆ4＋ｆ5−ｆ7−２ｆ8−３ｆ9−・・・＝１２

の条件の下の放電（電荷の移動）に帰着させる（放電法）のであるが，この手続きにはどうしてもコンピュータが必要になったのである．

　アペルとハーケンの後も放電法の改良が続けられ，１９９４年，ロバートソン，サンダース，シーモア，トーマスの４人が新たな１章をつけ加えた．しかし，これとて基本的にはアペル，ハーケンと同じコンピュータ路線なのであって，その証明は改良されてかなり簡単になったとはいえ，いまだ手計算で証明を完成させた人はいない．

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

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

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