ロビン・ウィルソン『四色問題』（茂木健一郎／訳）

 ロビン・ウィルソン『四色問題』（茂木健一郎／訳）を図書館で借りて読んでみました。この問題は100年以上も数学者を悩ませていましたが、1970年代にコンピュータを利用して証明されたそうです。「コンピュータを利用して証明された」とはどういうことなのか気になりました。その書籍には具体的なことは、あまり書かれていませんが、関係ありそうな箇所を拾ってみました。

• 【213頁】ちなみに、デュレがこのとき利用したコンピュータはハノーファー大学のCDC1604Aで、プログラミング言語はALGOL60だった。
• 【218頁】ハーケンは、ヘーシュとデュレを助けるため、イリノイ大学のILLIAC-IVというパラレルスーパーコンピュータの使用を申請したが、コンピュータは未完成で、使える状態になっていなかった。
• 【220頁】ブルックヘブンでは、デュレは最初にALGOLのプログラムをFORTRANに書き換えなければならなかったが、（後略）
• 【239頁】彼らは、一つの配置をチェックする時間を形式的に制限して、IBM370-158コンピュータでは90分、IBM370-168コンピュータでは30分でチェックを打ち切ることにした。

このように当時のコンピュータ環境が窺えます。その計算に長時間を要した（「どんな結果が出るか分からないような状況で1200時間もコンピュータを使用させてくれる研究所など、普通なら考えられない」と239頁に書かれています）ようですが、 それは当時のコンピュータの技術水準での話です。

数学上の難問をコンピュータで証明したというのが、いったいどういう意味なのか掴みかねます。さらに、その計算に何百時間も要しているという事実も、その問題の難しさを語る事情を補強する材料になっていないでしょうか。当時のコンピュータでは何百時間も要したかもしれませんが、今日のコンピュータなら数十分かもしれません（最近話題の量子コンピュータなら一瞬かもしれません）。