＃又吉直樹のヘウレーカ 1/9は”4色ボールペンって便利なの？”で四色問題を題材にしていました。地図は飛び地があるので5色とか。速記メモ。

解説は東工大の鈴木咲衣さんでした。

http://www.is.c.titech.ac.jp/~sakie/sakietech/homu.html

アッペルとハーケンの論文はこちらなどで読める。

Every planar map is four colorable.　Part I and II

https://projecteuclid.org/euclid.ijm/1256049011

https://projecteuclid.org/euclid.ijm/1256049012

もっと新しい形式的証明のCoqをつかったものはこちら。

"A computer-checked proof of the Four Colour Theorem"

http://www2.tcs.ifi.lmu.de/~abel/lehre/WS07-08/CAFR/4colproof.pdf

では以下速記メモ。

---

又吉さんが文具店でボールペンを選んでいる。

そこに鈴木咲衣さんが登場。お勧めは4色という。3色だとちょっと足りないって。

4色あるということが数学的には大事だという。

実は2017年に番組に出てた。

NHK又吉直樹のヘウレーカ！を観てました。千葉逸人さん、鈴木咲衣さん登場の数学の番組で、メトロノーム同期・蔵本モデルが出てくる。速記メモ。 #ヘウレーカ #NHK

次に向かったのは荒川修作さんたちが手掛けた住宅。数学者が住んでいたこともある。

多様性がある感じがするという鈴木さん。

四色問題とは何か？を問われる又吉さん。

四色の中でどれが一番使われるのか？あるいは使われない色は？という問題？と答える。

そこに出てきたのは日本地図と色鉛筆。

色分けしていない地図の隣り合う県を塗り分けていくとき、何色あれば塗り分けられるか？

三色？と答える又吉さん。答えは四色。

隣り合う県や国を違う色で塗るには4色あれば十分。すでに証明されているので四色定理と呼ばれるはず。でも未解決の時間が多かったので、今でも四色問題と呼ばれる。

ということで実際に又吉さんが塗ってみる。

が、、、HiramekiLabのアプリを使うのが簡単ということでそれを使う。

four color

https://www.hiramekilab.com/services/fourcolor2/

そして地図に挑戦。

https://n.freemap.jp/tp/Japan

長野県以外は3色で塗れた。

こんな感じのやつは4色必要。

最初に気づいた人は？

紙芝居で示す。

150年以上歴史がある問題。

1850年台、ロンドンでド・モルガンはハミルトンに手紙を書いた。

フレデリック・ガスリーという学生から地図は四色で塗れるかを聞かれたと。そのお兄さんのフランシス・ガスリーが気付いていたという。

そして120年以上のち、アッペルとハーケンが証明したと発表した。

計算にコンピュータを使っていたので大きく取り上げられた。

しかし、一部の数学者からは批難を受けた。証明がエレガントではないと。

証明を誰でもチェックできることが数学で、チェックできないのはだめだと。

しかし今はコンピュータによる計算をまたコンピュータにチェックさせる形式的証明も出てきた（上のリンクにつけたCoqのやつ）

ハッブルとハーケンの結果を積み重ねると1.2mくらいの紙になるという。

人間に全ての段階がチェックできないようなものは証明としてどうなんだ、という考えもある。

しかし何か根拠を持って正しいと言えたというのが大きな進歩ではないかと語る鈴木さん。

イラストレータの渡辺裕子さんが登場。顔はお面で隠しながらまとめのイラストを。

100年以上未解決問題としてあったおかげで色んな議論が生まれたが、その脇道でいろんな数学の発見があった。

それを考えたことによって鍛えられた思考が別の問題を解決する、という又吉さん。

考える過程で生まれたもの。

地下鉄の路線図はグラフ理論を使っている。

日常生活の中にも数学が潜んでいることがある。

数学の種、四色問題の種を鈴木さんが探す。なぜか探偵のファッションで。

向かったのは地図の出版社。

カラフルなアートのようなものを見せられる。

町ごとの地図の塗り分けを濃くしたもの。透明度を上げると北海道札幌の地図でした。

5色を使っているそうだ。小さな町だと飛び地がある。同じ町名は同じ色にするという原則があるので、5色にしている。

感覚的にそうだろうな、とわかる段階と数学的に証明する段階の間には大きな差があると語る鈴木さん。

数学の証明とは何だと思う？問われる又吉さん。

道筋？と答える又吉さん。

ある事柄は正しいことを、すでに正しいと認めらている前提や過程から導くこと

ということだと答える鈴木さん。

別の証明の仕方をしても論文になるという、より多くの人に理解されやすいものなど。

数学の証明にはパターンがある。

背理法を説明する。

何か濡れ衣を着せられたことがある？と聞かれる又吉さん。

バイト先でお金がなくなったりした、、、というシリアスな話。

やってませんよ、と説明して防犯カメラを確認したらいいんじゃないですか？といっても疑われる。それでシフトから名前が消えた、、、

そういう時に役に立つかもしれない背理法。

プリンが出てきた。

又吉さんのお姉さんが電車で一時間で住んでいるとして、たまに遊びに行く仲とする。

プリンを食べたでしょ！と電話がかかって来たとする。

家にいってないということを証明する、と答える又吉さん。

証明したい主張を一度否定し、そこから矛盾を導くことで真実を引き出す。

まずプリンを食べたと仮定する。

するとお姉さんの家に行ったことになる。

電車で1時間かかる。プリンを食べるには2時間不在になる。

だが、その時間仕事をしていた。

なので矛盾している。

ということで証明される（とコナンくんのBGMに乗せて、、、）

では又吉さんの主張を。

「ぼくは、カレーが好き。」

背理法で証明する。

僕はカレーが好きでないとするなら、なぜ昨日カレーを食べたのか、カレー好きをアピールするのに食べたのか？

応援したいから食べた。

一人で食べにいったのか？応援にならないんじゃないのか？

とか鈴木さんに詰め寄られる又吉さん。

これが背理法？

そしてコーヒーを入れる。ググってやり方を調べたという鈴木さん。

2人でプリンを食べながらコーヒーを飲む。

裏側だけ食べる又吉さん。色んな角度から見られる数学的な食べ方、、、

締め切りが1つなら集中できるが、一杯あると何も手につかない、できることからやっていけば実は全部できる、ということを今日の話で感じたという又吉さん。

これを全部終わらせることは無理、という背理法。

（なるほど）

又吉さんも4色ボールペンで小説を書いたら？という鈴木さん。

数学の玄関が見えたかも、という又吉さん。いつかドアを開けて、、、

---