ぬりわけの ルールは、「さかいの 線が つながって いる となりどうしは、ちがう 色に する」です。さかいが 1てんだけで ふれあって いる ところは、となりとは かぞえません［1］。

この ルールで ちずを ぬると、1色や 2色では たりない ことは すぐ わかります。じゃあ、3色では どうでしょう。 下の ずの ような ちずを かいて みましょう。まるい 大きな ちずを 3つに わけ、その まわりを ぐるっと かこむ わっかを 1つ つけます。4つの ばしょは、どれも どれとも さかいが くっついて いるので、ぜんぶ ちがう 色が 必要ひつようです。だから 3色では たりません。

では 5色は いるのでしょうか。いいえ、ちがいます。どんなに ふくざつな ちずでも、4色で ぬりわけられます。（1つの 国が はなれた ところに ある ばあいは、べつの はなしです。）これが 四色問題よんしょくもんだいの こたえで、いまは「四色定理よんしょくていり」と よばれて います［1］。

塗り分けのルールは、「境界線を共有する領域どうしは、別の色にする」です。点で触れ合っているだけの領域は、隣とは数えません［1］。

3色では足りない地図は、簡単に作れます。円を3つの扇形に分け、そのまわりを輪でぐるりと囲みます。扇形A・B・Cと外側のDは、どの2つも境目で接しているので、4つとも別の色が必要です。だから、最低でも4色は要ります。

では、5色や6色が要る地図はあるのでしょうか。答えは「ありません」です。平面や球面に描いたどんな地図も、4色で塗り分けられます。（国が1つにつながっている地図の話で、離れた土地を同じ色にしたい場合は別です。）これが四色定理で、現在は証明されたものとして扱われています［1］［2］。

ただし、この「4色で足りる」を証明する道のりは長く、途中には、一度「証明できた」と信じられた説が間違いだった事件もあります。

塗り分けのルールは、「長さのある境界線を共有する領域どうしは、別の色にする」である。点（角）で触れ合うだけの領域は隣とみなさない［1］。

3色で足りない地図は簡単に作れる。円を3つの扇形に分け、そのまわりを輪で囲む。扇形A・B・Cと外側のDは、どの2つも境界で接するので、4つとも別の色が必要だ。したがって最低4色は要る。

では5色以上が必要な地図はあるのか。平面（球面）上のどんな地図も4色で塗り分けられる、というのが四色定理で、1976年の発表を経て、現在は定理として受け入れられている［1］［2］。ただし、地図が平面でなければ話は変わる。ドーナツ型（トーラス）の面では、7色が必要になる地図がある［1］。また、同じ国の離れた土地（飛び地）を同じ色にしたい場合も、4色では足りなくなる地図がある［2］。

題名の後半の問い、つまりコンピューターが関わった証明をどう受け止めるかは、後ろの章で扱う。その前に、疑問がどう生まれ、どこでつまずいたかを見ておく。

はじまりは、1852ねんの イギリスです。フランシス・ガスリーと いう 学生が、イギリスの ちほうごとの ちずを ぬっていて、気が つきました。「4色で たりそうだ」と いう ことです［3］。

ガスリーは、弟の フレデリックに この ぎもんを はなしました。フレデリックは 数学の 先生の ド・モルガンに たずねます。先生は、10月23日に 友だちの 数学者 ハミルトンへ てがみを かいて、この ぎもんを しらせました［3］。

ぬりえの ようだけれど、数学では 「何しゅるいの ちずでも」を しめさなければ なりません。ためした ちずが 1000まい あっても、1001まいめで だめかも しれないからです。

問いの始まりは、1852年のイギリスです。フランシス・ガスリーという学生が、イギリスの郡の地図を色分けしていて、「4色で足りそうだ」と気づきました［1］［3］。

ガスリーはこの疑問を弟のフレデリックに話し、フレデリックは自分の先生だった数学者オーガスタス・ド・モルガンに尋ねました。ド・モルガンは1852年10月23日、友人の数学者ハミルトンに宛てた手紙でこの問題を知らせています［1］［3］。

ぬり絵のように見えても、数学で「どんな地図でも」を言うには、すべての地図について言える理由が必要です。1000枚の地図で試して大丈夫でも、1001枚目で失敗するかもしれないからです。ここから、四色問題の証明を探す試みが続きました。

始まりは1852年のイギリスだ。学生フランシス・ガスリーが、イングランドの郡の地図を塗り分けていて、「4色で足りそうだ」と気づいた［1］。ガスリーは弟のフレデリックにこの疑問を話し、フレデリックは自分の教師だったオーガスタス・ド・モルガンに尋ねた。ド・モルガンは1852年10月23日付で、友人の数学者ハミルトンへの手紙でこの問題を知らせている［1］［3］。

地図を何枚塗り分けても、証明にはならない。数学で「どんな地図でも」を主張するには、すべての地図に通用する論理が要る。試した地図が1000枚でも、1001枚目で行き詰まる可能性が残るからだ。この問題は、そのあと100年以上、数学者を悩ませ続けた。

1879ねん、ケンプと いう 人が 「しょうめいできた」と はっぴょうしました。みんなは よろこびました。ところが 1890ねん、ヒーウッドと いう 数学者が、その しょうめいに あなが あることを みつけました［3］。11ねんも かかりました。

ヒーウッドは、がっかりしただけでは ありませんでした。ケンプの 考えかたを つかうと、「5色なら かならず たりる」ことは しょうめいできると しめしたのです［3］［1］。

4色と 5色は、たった 1色の ちがいです。でも、4色を しょうめいするのは、そこから 80ねん いじょうも かかる ことに なります。

1879年、アルフレッド・ケンプが証明を発表しました。『ネイチャー』という雑誌に1879年7月17日に載り、同じ年にアメリカの数学雑誌にも発表されます［3］。多くの数学者が、これで解決だと考えました。

ところが1890年、パーシー・ヒーウッドがケンプの証明の誤りを示しました。ヒーウッド自身は、自分の論文を「建設的というより破壊的」と書いています［3］。誤りが見つかるまで11年かかったのです。

ただし、ヒーウッドは壊しただけではありません。ケンプの方法を使えば、「どんな地図も5色で塗り分けられる」ことは証明できると示しました［3］［1］。4色と5色の差は1色だけですが、その1色をなくすのに、そこから80年以上かかりました。同じころの1880年にはテイトも証明を発表しましたが、こちらも1891年にピーターセンに誤りを指摘されています［1］。

1879年7月17日、アルフレッド・ケンプが『ネイチャー』誌上で証明を発表し、同じ年にアメリカの数学雑誌に論文が載った［3］。広く称賛されたが、1890年にパーシー・ヒーウッドが誤りを指摘した。ヒーウッドは自分の論文を「建設的というより破壊的」と評している［3］。誤りが見つかるまでに約11年かかったことになる。1880年のテイトの証明も、1891年にユリウス・ペーターセンが反論を示した［1］。

ヒーウッドは壊すだけでなく、ケンプの方法の核を使って、「どんな地図も5色で塗り分けられる」ことを証明した（五色定理）。あわせて、問題を任意の種数の曲面に広げ、トーラスなどでの必要な色数の予想（ヒーウッド予想）を出した［3］［1］。この予想は、1968年にリンゲルとヤングスらによって証明された［1］。4色と5色の差は1色だが、その1色の壁は、1976年まで破られなかった。

1976ねん、アメリカの イリノイ大学の アッペルと ハーケンが、ついに 4色で たりる ことを しめしました。ここで つかったのが、コンピューターです［1］［3］。

やりかたは、こう です。どんな ちずにも、かならず あらわれる 「ちいさな かたち」の リストを つくります。つぎに、そのリストの かたちが ある ちずは、かたちを ちぢめて ちいさな ちずに かえても、4色で ぬれる ことを たしかめます。リストの かたちは 1500こ ほど ありました［3］。1つずつ しらべる のは、人では とても できません。

コンピューターは およそ 1200じかん、はたらきました［3］［2］。そして、「どんな ちずも 4色で ぬれる」と いう 答えが、でました。はじめに 書いた 「FOUR COLORS SUFFICE」の はんこは、この ときの ものです［1］。

1976年6月21日、イリノイ大学のケネス・アッペルとウォルフガング・ハーケンが、四色問題を解いたと発表しました［1］。決め手は、コンピューターを使った証明でした。

考え方はこうです。もし4色で塗れない地図があるなら、そのうち一番小さいものを考えます。そこで2つのことを示します。1つは「どんな地図にも、リスト（不可避集合）のどれかの形が必ず含まれる」ということ。もう1つは「リストの形が地図に含まれているなら、もっと小さい地図の塗り方から4色の塗り方が作れる（可約）」ということです。すると、「一番小さい」という仮定に反するので、4色で塗れない地図はない、と言えます。リストの形は1500ほどありました［3］。

この大量の確認に、コンピューターが約1200時間使われました［3］［2］。人が手で確かめるには多すぎ、同じ年のイリノイ大学の郵便物には「FOUR COLORS SUFFICE」のスタンプが押されました［1］。

アッペルとハーケン（イリノイ大学）は、1976年6月21日に四色問題の解決を発表した［1］。証明の骨格は、「最小反例」を考える背理法だ。4色で塗れない地図があるなら、領域の数が最小のものを取る。示すべきことは2つある。

• 不可避性：どんな（最小反例にあたる）地図にも、あるリストの「配置」のどれかが必ず含まれる（不可避集合）
• 可約性：その配置を含む地図は、配置の部分を縮めた、より小さい地図の4色塗りから、4色塗りを作れる（可約）

すべての不可避な配置が可約だと確かめられれば、最小反例は存在できない。不可避集合の配置は1500ほどで、可約性の確認だけでも1834個を調べ、のちに1482個に絞られたとされる［3］［1］。計算には約1200時間のコンピューター時間が使われた［3］［2］。不可避性を示す部分は、400ページを超える資料になった［1］。

この年、イリノイ大学数学教室の消印は「FOUR COLORS SUFFICE」になった［1］。手作業で調べる部分は約1万の場合分けにのぼり、小さな誤りがいくつか見つかっていた［4］。1989年には、全体をまとめた本が出ている［1］。

この しょうめいは、人が ぜんぶ 読んで たしかめる ことが できません。そのため、すうがく者の あいだで、「これは しょうめいと いえるのでしょうか」と いう 話に なりました［1］。

それから、ほかの 人たちが べつの プログラムで たしかめたり、しょうめいを かんたんに したり しました。1990ねんだいには、ロバートソンさん たちが、べつの しょうめいを つくり、しらべる かたちを 633こに しました［5］［4］。

そして 2000ねんだいの はんばに、ゴンティエさんが、「コック」と いう ソフトで、しょうめいの 理くつの 1つ1つまで、きかいに チェック させました［4］［1］。いまは すうがく者の おおくが、この しょうめいを うけいれて います。ただ、人が 読んで なっとくできる みじかい しょうめいは、まだ みつかって いません。

問題は、この証明を人が最初から最後まで読んで確かめることができない、という点でした。「コンピューターの結果を信じてよいのか」「プログラムの間違いはないのか」という疑問が、数学者の間に起こりました［1］。

そこで、確かめる仕事も進みました。1990年代にロバートソン、サンダース、シーモア、トーマスの4人が、リストの形が633個の、より簡単な証明を作りました［5］［4］。それでも計算はコンピューターが行います。

さらにジョルジュ・ゴンティエは、2000年代の半ばに、「Coq」という証明検証用のソフトで、この証明の論理の1段ごとを機械に検査させました［4］［1］。この方法なら、頼るのは検査用ソフトの小さな部分だけで済みます［1］。

いま、多くの数学者はこの証明を受け入れています。ただし、人が読んで納得できる短い証明は見つかっておらず、「証明とは何か」という問いは、四色定理から広がって残っています。

最大の論点は、人が全体を追えない点にある。計算機が出した結果の正しさは、プログラムとハードウェアの正しさに依存する。1976年の証明には実際に手順の誤り（1980年代前半に発見・修正）もあり、疑いはもっともだった［1］。

確かめる側の仕事も進んだ。1990年代にロバートソン、サンダース、シーモア、トーマスが、配置が633個の、より簡単な証明を示した（論文は1997年1月に改訂）［5］。基本の考え方はアッペルとハーケンと同じで、計算機が欠かせない点も変わらない。

そこで次の段階として、ジョルジュ・ゴンティエが2000年代半ばに、定理証明支援系「Coq」を使ってこの証明を形式化し、論理の各段階を機械で検査した［4］［1］。検査では、小さなプログラム（カーネル）が論理の手順を確かめる。検査全体の正しさは、この小さなプログラムに頼る［1］。

この結果、証明そのものは多くの数学者に受け入れられた。一方で、人が読んで理解できる短い証明はまだ知られていない。「理解できなくても、証明は証明か」という問いは、四色定理から数学全体に広がった論点になっている。

しろい ちずを 1まい よういして、いろえんぴつを 4ほん だけ つかって ぬって みましょう。となりどうしが ちがう 色に なれば せいこうです。

さいしょは かんたんな はずが、ちかい ところから ぬり すすめて いくと、とちゅうで 「あれ」と なる ことが あります。そのときは、ぬりなおす 場所を さがして みましょう。むかしの 人が まよった ところを、ちょっとだけ たいけん できます。

白地図を4色で塗ってみる

白地図を1枚用意して、色鉛筆4本だけで、隣どうしが別の色になるように塗ってみよう。途中で詰まったら、色を塗り替える場所を探してみましょう。ケンプが考えたのも、そういう塗り替えでした。

3色で足りない地図を描く

この記事の図のように、4つの領域が全部、互いに接する地図を自分で描いてみましょう。5つの領域が全部互いに接する地図は、平面では描けないことも試せます。

原典に当たる

St Andrews大学の数学史サイト「MacTutor」には、四色問題の歴史がまとまっています［3］。ゴンティエの報告は、機械に検査させる体験が書かれています［4］。

白地図を4色で塗ってみる

白地図を4色で塗り分けて、行き詰まったときにどう塗り替えれば抜け出せるかを考える。ケンプの証明が使った「塗り替え」の発想を、体験できる。

なぜ5つの領域が全部接する地図は描けないのか

3色で足りない地図（4つが互いに接する）は描けた。5つの領域がどれも互いに接する平面の地図は描けるだろうか。実際に描いてみて、描けない理由を考えてみる。五色定理の証明の入口にもなる。

原典に当たる

MacTutor（セント・アンドルーズ大学の数学史サイト）の四色定理の項目で歴史を［3］、ゴンティエの報告で形式証明の実際を読める［4］。