5. 4色定理とコンピュータ
4色定理とは平面上に地図が書かれていてその国に色を塗るとき, どんな地図でも4色あれば足りるという定理である(一つの国は飛び地を持たないとする). これを証明するのにコンピュータが用いらた。この事について数学者(+世間の人たち?)の間で, 「コンピュータを用いたを証明と呼べるのか」という議論がなされたという事は聞いたことがあるかもしれない.
コンピュータが用いられたといっても, 決してありとあらゆる地図に対する塗りわけをコンピュータにやらせた, というものではない. 地図の種類は無限にあるので, そんなことは不可能である. そして, 意味のある数学の定理は事実上全てが, 無限の対象に対する言明(全ての自然数は..., 全ての実数は...)だから, コンピュータによって「難しい」定理の証明の 「本質的な部分」がなされる可能性は今も昔も少ない.
4色定理の場合まず, 何通りかの「部分地図」の形が定義され,
- どのような地図も必ずそれらのうちのどれかを一部に含む
- 一方, それらのどれも, 4色で塗り分けられない最小の地図(最小反例)には含まれ得ない,
上で何通りかの「部分地図」と述べたその部分地図の数が, 最初の証明(AppelとHaken)では1476種類あり, 前者の証明やプログラムも複雑であったため, その正しさに疑問がつけられたという. 後にThomasらによってより単純なプログラムによる証明が得られ, その際の「分類」の数は633種類だった.
参考リンク:
私自身はコンピュータをやっている人間として, このような証明がなされたことに興味を覚えるし, 今後別の, もっと多くの数学者の関心を引いている問題で, 似たようなことが起きても不思議はないと思う。むしろそれが数学の進歩に役に立つのであれば喜ばしいと思う. そもそも命題自身の真偽がわかっていない状態では手段など選ばず, 「後はこれら有限個の場合をコンピュータでチェックするだけ」というところに持ち込んだら, コンピュータを利用するのは自然なことだ. そして4色問題を「有限個の場合のチェックを行えば良い」ところまで持ち込んだのは紛れもなく人間だ。今後別の問題の場合でもおそらくなるするだろう.
これに対し, 「これを数学の証明と呼べるのか」という批判が起きるのもまた分からないこともない. 要するに証明は「白黒つける」だけが目的ではなく「分かる」事が目的であり, 要するに何を持って「分かった」とするかという問題だ. コンピュータの手続きがYESと答えたからと言って, それを見た人にとって「分かった」という満足が得られないではないかという感覚は理解できる. しかし, チェックのためのプログラムが十分理解可能で信頼に足るものであれば, 「わかった」と言えるのではないか. そもそも人が書いた証明であればそれが1000ページを越えており, 自分ではとても検証できなくても良しとするというのも不思議な話だ. 要するにプログラムを使うと「分かった」とは言えず, 使わなければ「分かった」というような 2者択一ではないということだ.
そもそも同じ問題に何通りも証明があるのが普通であり, その問題が重要ならば, たとえ先にコンピュータを用いた証明がなされたとしても, より簡潔な, うまくするとコンピュータに頼らずに正しさが確認できるような別証が出てくるのが普通だろう. それは他の問題でも, 最初に長く複雑な証明が提出された後, より本質をついた, 整理された証明が出てくるのと同じ事だ. たまたま最初になされた証明がコンピュータを使った「人」によってなされたというに過ぎない. それを認めずに「コンピュータに先を越された」とか, 「コンピュータに人間が負けた」という類の感情論はナンセンスだ. そのような人にはぜひ以下の事実を思い起こしてもらいたい. コンピュータによる計算の原理も, その物理的な実現方法も, プログラムによる計算の表現方法も, 元はと言えばすべて人間が考えたものだ.
出典：Motivation to learn computer (一部変更)
0 件のコメント :
コメントを投稿