数学者とコンピュータ、補い合ってめざす思考の頂

鈴木 正明（明治大学 総合数理学部 教授） AIをはじめとする情報処理技術は日進月歩の速さで進歩し、ビジネスからクリエイティブまでさまざまな分野で存在感を増しています。人間の思考のひとつの極致ともいえる数学の世界でも、半世紀も前からコンピュータ（計算機）が使われていることはご存知でしょうか。数学者はどんなふうにコンピュータを使いこなし、コンピュータは数学にどんな影響を与えてきたのか、その歴史と現在をひもときます。

◇半世紀前、コンピュータを使って初めて証明された「四色問題」 数学の研究というと、紙と鉛筆で計算したり、黒板に難しい数式を羅列したりするイメージをもつ方が多いかもしれません。もちろん、現在もそのようなスタイルで研究を行っている数学者は多いですが、その一方でコンピュータの登場によって研究手法が大きく変わった側面もあります。手計算ではできなかったような膨大な量の計算が可能になったのはもちろんのこと、計算結果をグラフなどで視覚化することも簡単にできるようになりました。一見して複雑な式でも、コンピュータを使ってグラフを描くことでその性質が理解でき、それによって研究が進展することもあります。 コンピュータを使った数学研究でエポックメイキングになったのは、「四色問題」と呼ばれる問題でした。これは、「平面上の地図は4色で塗り分けることができる」という命題が正しいかどうかを問うものです。例えば、日本地図の都道府県を色鉛筆で塗り分ける場合を考えてみましょう。実際にやってみると、4色の色鉛筆があれば隣り合う県同士が同じ色にならないように塗り分けられることがわかります。このように、およそどのような地図でも4色あれば塗り分けられることは古くから経験的に知られていたのですが、数学的にこれが正しいと言うためには、無限通りありうる地図のすべてでこの性質が成り立つことを証明しなければなりません。 数学者ド・モルガンが1852年に書いた手紙の中で提起して以来、長年にわたって数学者たちを悩ませてきた四色問題ですが、1976年にアッペルとハーケンという数学者がコンピュータを使って解くことに成功し、どんな地図でも4色で塗り分けることができるという結論が導き出されました。 彼らは一体どのような方法で四色問題を解決したのでしょうか。いくら優れたコンピュータでも、無限通りの地図のすべてを計算することは不可能です。彼らが行ったのは、高性能なコンピュータの計算能力を使って無限通りの地図を約2000のパターンに場合分けし、そのひとつひとつの場合について、4色で色分けが可能かどうかを人力でチェックすることでした。もちろん、場合分けのために必要なアルゴリズムは彼ら自身が作り上げたものです。 数学の証明にコンピュータを用いることは当時としては先進的なことでした。コンピュータの計算が果たして常に正確なのかはいわばブラックボックスで、人間の目からは検証が困難なため、その結果を信じてもいいのかどうかには賛否両論があったようです。ともあれこれ以降、数学の証明にコンピュータが用いられる例が増えてゆき、コンピュータの性能の向上とも相まってその成果が受け入れられるようになってゆきました。しかし、人間が100％責任を負うことのできない計算結果を数学の定理としてよいのかどうかは、数学者の間でもいまだに意見が分かれるかもしれません。 ちなみに、アッペルとハーケンがコンピュータを用いて行った証明は、のちに別のプログラムでも検証されてその正しさが確認されていますが、コンピュータを使わない証明はいまだに発見されていません。