とある数学の四色問題

『数学ガール/ゲーデルの不完全性定理』を読んだ。
本書は『数学ガール』、『数学ガール/フェルマーの最終定理』に続くシリーズ3作目。

後半、大量の定義が現われるところで、迷子になった。
読んでいる最中はは面食らったけれど、冷静に考えると、リファクタリングの一つ『メソッドの抽出』を行う理由はここから来ているのだろうな、と思った。

例えば、

省略系4 ∃_x(a) を ￢(∀_x(￢(a))) と定義する。

いちいち"￢(∀_x(￢(a)))"を使っていると、全体を読み通すのが困難になる。
かと言って、"∃_x(a)"の定義を把握していないと、それが"￢(∀_x(￢(a)))"の省略系であることを逐一確認しないといけない。

リファクタリングの文脈で言い換えるとこうなる。
適切にメソッドを定義しないと、ソースコードの全体の流れを把握できなくなる。
一方で、メソッド過多でも、 ソースコードの見通しが悪くなる。定義を把握していないメソッドが出てくる度に、定義を確認する必要が生じる。

本書の後半は、今の自分のキャパシティを越えていた。
もう少し定義を丁寧に追いながら読んだら、理解が深まるだろうか。
あるいは少し手を動かした方がいいかもしれない。




ところで、コンピュータと数学と言えば「四色問題」を思い出す。

『四色問題』を読んだ範囲での理解だと、『ゲーデルの不完全性定理』ほどではないかもしれないけれど、これも当時の《数学観》に《ガリレオのためらい》を与えたんじゃないだろうか。

《ガリレオのためらい》を与えたのは、証明の方法。
人間の手には終えない数の場合分けを、コンピュータで実行した。

確かに、オイラーの公式のような一種の美しさを感じない。
しかし、 コンピュータで実行できるように問題を定式化するのも、十分チャレンジングだ。
（テトラちゃんのように）数え上げるのも立派な数学だと思う。
それに、定義、公理、推論規則から引き出される結論なら、それは数学だ、と思う。