|
同じくパソコンで証明されたという記事を見つけました。。。^^
「September 30, 2005 ジョルダン曲線定理、世界初の完全証明
フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤りなどを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が完成。中村教授らは「完全証明したのは世界初」としている。
「ジョルダンの曲線定理」は「平面上の閉じた曲線は、平面を曲線の内と外に分ける」というもの。直感的には明らかだが、数学的な証明は難しいとされてきた。
中村教授によると、人間が行った数学的な証明をチェックする「プルーフ・チェッカー」というコンピューターシステムのうち、今回はポーランド・ビアリストーク大のアンジェイ・トリブレッツ博士（６４）らが開発した「ＭＩＺＡＲ（ミザール）」と呼ばれるシステムを使用したという。中村教授は「同様のシステムでコンピュータープログラムにミスがないことを確認するなど、今回の成果は実社会にも応用できる可能性がある」と話している。
・・・
紙の上に鉛筆で一筆の適当な線を描きます。画像
線が途中で交わったりしないようにし、出発点に戻ってくるようにすると、きちんとした閉じた図形が出来上がります。このとき、この図形によって「必ず」内側と外側にきっちり分けられるのだろうかというのが、ジョルダンの閉曲線の定理とされているものです。
私たちは感覚的に、そんなことは明白じゃないか！と思うわけです。
何回やってみても、どんな形になろうとも、描かれた閉曲線によって二つの領域に分かれることを当たり前のこととして学習しているからです。しかし、いざそれを数学的に証明しようとすると、とてつもない困難に突き当たります。たとえ、何千万、何億回繰返して検証したとしても、たった一つの成立たない事例が見つかるかもしれない。そういう可能性が無いという事は否定でないからです。
当たり前だと思われている事が、実は感覚的という危うい前提の下に成り立っているということはとても多いのですね。
さて、そもそも、前提となる連続曲線って何でしょうか。
「一筆で書かれた連続的な線」という表現では不十分ですね。
とすれば、
実数の区間[0,1] からユークリッド平面上への写像として定義された線分
(x(p),(y(p)),0≦p≦1
が連続であるとは，任意の実数ε> 0 に対して，あるδ> 0 が存在し,|p'-p|<δならば
ρ((x(p'),(y(p'))-(x(p),y(p)))<ε
が成立すること．このような線分を２次元平面上の連続曲線と定義する。
とでも言わなければなりません。
そして、その連続曲線で作られる閉曲線については平面上の任意の２点が連続曲線で結ばれるとき、これを弧状連結と呼ぶ。
パラメータを0≦p≦1 としたときの閉曲線
(x(p),y(p)),(x(0),y(0))=((x(1),y(1)))
が途中で自分自身と交わらないとき、これを単純閉曲線という・・・・・・
というように、直感を排した数学を基礎から逐一構築していかないと、この定理の完全証明ができないのです。こういう途方ない作業を成し遂げて、完全証明を果たしたグループの皆さんに心より敬服いたします。」
http://e-learn.mine.nu/mizar/jordancurve.htm より Orz〜
JORDAN曲線定理の完全証明が完成！
「Camille Jordan が1887年に「この定理は明らかに成立する」と彼の著作の中で述べましたが、その後、この定理の証明は意外にむずかしいことが分かりました。Oswald Veblen が 1905年に一応の証明をしたと言われていますが、前提となる知識の到るところに直感が使われ、完全証明とは言いがたいものでした。他方多くの数学や科学の分野（複素関数論、電磁気学、４色問題）などではこのJORDAN曲線定理を暗黙にあるいは明示的に仮定していました。・・・
まず直感を排した数学を基礎から構築しないと、この定理の完全証明ができないことは明らかでした。たまたまコンピュータの発達を背景にしてプルーフチェッカーというシステムが登場してきました。これは定められた文法によって人が記述した数学の証明を、コンピュータがチェックする、というものです。コンピュータは融通が利かないので、そこに直感が入りこむ、という余地はありません。そのプルーフチェッカーで、世界で一番有名なものは、ポーランドのA.Trybulec博士らのチームによって作られたＭＩＺＡＲとよぶシステムです。日本の中村八束も独自のプルーフチェッカーを作りましたが、ポーランドのチームに合流して、ＭＩＺＡＲの大きな仕事として、JORDAN曲線定理の完全証明を一緒に、日本とポーランドの共同プロジェクトとして行うことを提唱しました。これが１９９１年のことです。・・・そして２００５年９月にArtur Kornilowicz博士によって最後の部分が完成し、１４年間に渡ったこのプロジェクトは成功のうちに幕を閉じたのです。
分担された部分の証明を合計すると、実に２０万行を要しました。これは論理的推論がいかに大変かを示すと共に、そのひとつの頂点を極めた、という意味でＭＩＺＡＲの可能性を示すものです。今後、この証明完成を契機として、ＭＩＺＡＲは新しい数学的手法あるいは数理的手法として世界に認知されてゆくでしょう。」
ま、よく分かりませんけど、、、数でも図形でも基本的な性質（直感的に明らかな）の証明ほど困難だってことは分かりますね。。。案外脳が当たり前だと思ってしまってるような（でも当たり前じゃないっていう）事柄に気付かないままそれを前提にして話が進んじゃってることってもっとあるのかも知れない、、、けど、、、数学者っていうとことん疑問に感じる人々がいる限りその危うさに足元をすくわれることから免れてるのかも知れないですね。。。^^;v
それにしてもこの関連記事が少ないのはなぜなんだろ・・・？
|
コメント（0）
