＼当サイトではリンク広告を利用しています。／
今日のテーマは、数学の難問「四色問題」。
1976年にコンピュータを用いて解決されたこの問題、実は「美しくない証明だ」と批判されてきました。
でも本当にそうなの？ちゃんと反論や進歩もあるんです。
ということで今回は、
こんな切り口で、数学の世界をちょっとだけ覗いてみましょう！
まずはおさらいから。
四色問題（Four Color Problem）とは：
「どんな地図でも、4色あれば、隣り合う国を違う色で塗り分けることができるか？」
という命題。
隣接する国は同じ色にできないけど、4色あれば必ず塗り分けられるのか？という素朴な疑問です。
数学者たちはこの問題を100年以上かけて悩み、議論し、時に諦めかけながら取り組んできました。
そして、時は流れ、1976年。
アメリカの数学者ケネス・アペルとウォルフガング・ハーケンが、
コンピュータを用いて四色問題の一般的な正しさを証明します！
彼らはまず、あり得る地図の形を1936の「還元可能な構成」に分類。
それをコンピュータで1つずつ検証することで、
「例外がないこと」を証明しました。
これにより、「四色問題は正しい！」と数学界に一応の決着がついたのです。
「😟 でも…この証明、美しくない？」
証明が正しいにもかかわらず、多くの数学者は違和感を覚えました。
その理由は、次のような批判によるものでした。
四色問題の証明が美しくないという批判を見ていきましょう。
証明には大量のコンピュータ計算が使われました。
しかし、1970年代のコンピュータは今ほど信頼性が高くありません。
といった問題が、見落としを引き起こす可能性があったのです。
数学の証明は、原理的に「絶対の信頼性」が求められます。
それに対して、「ソフトウェアのバグで証明が崩れるかも」というのは致命的な懸念でした。
証明に必要なデータ量が膨大で、人間の目ではすべてチェックできない。
つまり、「納得したくても見れない」状況が発生していました。
これに対して、
「それって、もはや“数学的証明”じゃなくない？」
という批判が噴出したのです。
「コンピュータは“確認”をしたかもしれないが、証明とは人が理解できる論理の構造だ」
というのが保守的な数学者の立場でした。
数学者たちは長年、論理と理論だけで証明を組み立ててきました。
それはまるで、芸術のようなもので、
そんな「美しい証明」を理想としていたんです。
しかし、当然ながらこれらの批判には強力な反論もあります。
まず、「バグがあるかも」という懸念は時代背景によるもの。
現代のコンピュータは桁違いに信頼性が高く、
再現性のある検証が世界中の研究者によって何度も行われています。
特に、ソースコードをオープンにし、
誰でも同じ条件で確認できるようにすることで、
「ブラックボックスではない」ことが証明の一部になってきているのです。
四色問題の初期証明では「1936通り」のケース分けが必要でしたが、
その後の研究により、
と、より美しく、論理的にも整理された方向へ進化しています。
つまり、初期は泥臭い brute-force 的な方法だったかもしれないけれど、
それも「入口」であり、今では「数学的に美しく整理された証明」へと発展しているのです。
そして意外かもしれませんが、四色問題の一部には、美しい論理的証明が存在します。
その代表例がこちら：
この条件下では、地図の構造が複雑すぎないため、
人間だけの手と論理で、四色塗りが可能なことが証明されています。
その後も研究が進み、「27か国」「30か国」と、
より大きなサイズでも人力証明が可能であることが示されてきました。
つまり：
という、実は両立する世界だったんですね。
この議論の背景には、そもそも
「証明における“美しさ”とは何か？」
という哲学的な問題があります。
人間が納得できるかどうか？
短くてエレガントな論理展開か？
それとも真理に到達するなら手段は問わないのか？
四色問題は、単なる数学的問いではなく、
数学という学問のあり方を問うた問題でもあったのです。
現代の数学では、コンピュータによる証明はむしろ当たり前になりつつあります。
定理証明支援ツール（Coq や Lean など）を使って、
論理の厳密性をコンピュータでチェックする時代が来ています。
それでも、やっぱり多くの数学者は、
「人間が見てわかる、美しい証明」を大事にしているんです。
四色問題のような例は、まさにその分岐点でした。
最後に、この記事の内容を箇条書きでまとめてみましょう！
数学って、ただの数字遊びじゃなくて、
人間の知の形や美意識まで問いかけてくる深〜い世界なんです。
次はどんな「美しい証明」と出会えるでしょうか？
それではまた次回！