【数学】ジョルダン曲線定理、世界初の完全証明＝信州大他

フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの数学者らが
完全証明に挑んできた「ジョルダンの曲線定理」について、信州大工学部の中村八束（やつか）
教授（６２）が２７日、ポーランドの数学者ら１６人との約１４年間にわたる共同作業で、
完全証明に成功したと発表した。
数式上の誤りなどを確認するコンピューターシステムのチェックを経て、約２０万行にわたる
証明が完成。
中村教授らは「完全証明したのは世界初」としている。

「ジョルダンの曲線定理」は「平面上の閉じた曲線は、平面を曲線の内と外に分ける」というもの。
直感的には明らかだが、数学的な証明は難しいとされてきた。

中村教授によると、人間が行った数学的な証明をチェックする「プルーフ・チェッカー」という
コンピューターシステムのうち、今回はポーランド・ビアリストーク大のアンジェイ・トリブレッツ
博士（６４）らが開発した「ＭＩＺＡＲ（ミザール）」と呼ばれるシステムを使用したという。
中村教授は「同様のシステムでコンピュータープログラムにミスがないことを確認するなど、
今回の成果は実社会にも応用できる可能性がある」と話している。

＠：http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html

証明は中村教授のホームページ（ｈｔｔｐ：／／ｍａｒｋｕｎ．ｃｓ．ｓｈｉｎｓｈｕ−ｕ．ａｃ．ｊｐ）で閲覧できる。

▽東京大大学院数理科学研究科・平地健吾助教授（解析学）の話
ジョルダン曲線のような、証明の難しい定理を、独自のシステムを使って検証したのは意義深い。
これだけの手間を掛けて、検証したことには驚きを感じる。
これまで知られている別の定理の証明を、このシステムで行うことも可能で、計算機科学の発展
に寄与すると思う。

やつか。カミーユ

計算機が出した結果が間違ってないことは、どうやって証明するのだろうか。
ーーー愚か者の疑問

ゴールドバッハ予想において大きな貢献を行ったエスターマンをして「頭のいい試み」と言わしめた
ジョルダン自身の証明から約120年。時代を感じるニュースです。

ニュースと直接は関係しませんが、四色問題の証明ではコンピュータによる証明を証明として
認めるべきか否かで論議をかもしましたが、今では証明の「検算」に貢献しているコンピュータ。
これもまた、時代を感じます。

平面上の閉じた曲線は、平面を曲線の内と外に分ける

あたりまえだろキチガイこんなの証明するまでもない他にやることあるだろうがｐｐｐ

>>5
こういう当たり前のことを証明することによって新しいことが見えてくるんだよ
たぶん

アドレス半角で書いてくれればコピペで飛べるのに。

証明は中村教授のホームページで閲覧できる。
http://markun.cs.shinshu-u.ac.jp/

URLは半角で記述しろよな

どうしてこれで証明された事になるか理解できない一般人にとっては禅問答
と同じだな。数学もようやく禅問答に追いついたか。

>>8
毎日は大文字なんですよ、いっつも。

計算機による検証付きの証明のことを
完全証明と呼ぶのですか？

内と外。意味がわからん。曲線といっても色々あるぞ。

>>7-8
すみません、悩んだのですが、新米でして改行以外の編集を加えるのに抵抗がありました。

この度の「完全証明」とは、中村教授のHPにあるように、「直感による説明を排除した証明」と
捉えられるかと思います。
数学における証明においては、「○○は自明である」と言ったような説明が多く、今回のケース
では、この中に直感を含む説明が含まれていたものを排除し、数学的・論理的に説明を行った
物であり、(直感の働かない)コンピュータによる検算によりその正しさが確かめられた、という
コトではないかと思われます。

どこで証明が見られるかわからなかった

>>12
○←閉じた曲線
∩←閉じていない曲線

この場合、真円だろうが楕円だろうがひょうたん型だろうがαだろうが何でもイイけど。

αは一寸まずいかと、、

>>13
多分計算機による証明チェックが初めてなされた、というだけかと思います
現代の数学において、直観的に明らかだからという理由だけで
〜は自明である、という「証明」がなされることは殆ど無いと思いますよ

反証されたんじゃないのか。つまらん。

　　　　　　　　　　　　　　　　　　　　　　　　 ,､ｧ
　　　　　　　　　　　　　　 　 　 　 　 　 ,､ '";ｨ'
_＿_＿＿___　　　　　　　　　　　　　 ／::::::/l:l
─- ､::::;;;;;;;;;｀ﾞﾞ''‐ ､　 　 __,,,,......,,,,_／:::::::::/: !|　　　　　またまたごｼﾞｮﾙﾀﾞﾝを
　　. : : : : : : ｀ﾞ'ヽ､:::ﾞヾ´::::::::::::::::::::::｀ﾞﾞﾞ'''‐'､. l|
､､ . : : : : : : : : r'":::::::::::::::::::::::::,r':ぃ::::ヽ::::::::ヽ!　　　　　　　　　　　　　　　　　,､- ､
.ヽ:ﾞヽ; : : : : : :ノ:::::::::::::::::::::;;､-､､ﾞ::: 　 　 rｰ-:'､　　　　　　　　　　　　　 　 ／　　 }¬､
.　＼::ﾞ､: : : :./::::::::::::::;､-''"::::::::::　　　,...,:::,::.,　:::':､　　　　　　　　　　　　_,,/,,　 ,､.,/ 　 }
　　　ヽ:ヽ､ /:::::::::::::::::::::::::　 　 　_　　｀ﾞ''‐''"　 __,,',,,,___　　　　　　　／~　　 ヾ::::ﾂ,､-/
　　　　 ｀ヽ､:::::::::;;;､､--‐‐'''''',,iﾆ-　　　 _|　　､-l､,},,　 ￣""'''¬-, '　 ''‐-､ .,ﾉ'ﾞ,i';;;;ﾂ
　　　_,,,､-‐l'''"´:::::::'　　,､-'" ,.X,_,,､-v'"''ﾞ''yr-ヽ / ﾞﾞ'ヽ､,　　　 ,.'　　　 　 jﾞ,,, ´　7
,､-''"　　 　.l:::::::::::;､-''"　 ,.-'　　ﾞ､""ヾ'r-;;:l　　冫、 　 　 ヽ､ /　 　 __,,.ノ:::::ヽ. /
　　　　　　　l;､-'ﾞ:　　 ,／　　　 　 ゞ=‐'"~ﾞﾞ')　./.　＼　　　　/　　'''"/::::;:::;r-''‐ヽ
　　　　　,､‐ﾞ ヽ:::::..,.r'ﾞ　　　　　　　　 ,,. ,r／ ./　　　 ヽ.　　 ,'　　 　 '､ノ''"　　　ﾉ
　　 ,､‐'ﾞ　　 　 ﾝ;"::::::.　　　　　　　"´ 'ﾞ ´　/　　　　　 ﾞ､　,'　　　 　 　 　 　 ／
　　'　　　　　／/:::::::::　　　　　　　　　　　　{.　　　　　 　 V　　 　 　 　 　 ／
　 　 　 　 ／ ./:::::::::::::　　　　　　　　　　　　',　　　　　　 /　　　　　　 　 /
.　　　　／　 /:::::::::::::::::.　　　　　　　　　　　　',.　　　 　 /　　 ,.､　　　　 /

ミザール　キカザール

ジョルダン標準形の人？

これってユークリッド空間の話？
非ユークリッド含むの?

乗換案内禁止

万年筆の試筆は曲線を書いただけでは
本当の書き味は解りません

あなたが普段書く文字を幾通りも書いてみて初めて解るのです

>約２０万行にわたる証明が完成。
>中村教授らは「完全証明したのは世界初」としている。

>「ジョルダンの曲線定理」は「平面上の閉じた曲線は、平面を曲線の内と外に分ける」
>というもの。 直感的には明らかだが、数学的な証明は難しいとされてきた。

山手線が内と外を分けるって約２０万行にわたる証明が必要なんだか｡驚々愕々｡

��当たり前�≠ﾈことを検証するのも、学問です。

冗ﾙ談だろ？

信州大工学部教授（６２）の言ってる「完全証明したのは世界初」と
東大数理研助教授の言ってることが完全に食い違ってるのにﾜﾛﾀ。

結局、4色問題だけが未だ取り残されている感じがするのは俺だけか?
エレガントでもなんでもないし。

俺の直線定理
《平面状の直線は右と左に分けられる》

誰か証明してくれ

平面状の直線の定義からだな。

これ公理じゃないのか
証明できると思わなかった。

>>29
上下もあるぞｗ

平面化の直線は右と左に分けられる

これはフィールズ賞は年齢的に無理だから、アーベル賞級ということ？

有権者は右と左に分けられる

じゃあ俺も
閉じた立体は内と外に分けられる

>>28
コンピュータを使った証明で、他に有名なものはケプラー予想もありますね。
結局、コンピュータを使った証明は、同時にコンピュータ使わなければ検証が難しいということでもあり、
これら、いわゆる力技といわれるような証明は今後も多々でてきそうですね。

直線と言うことであれば、
y=ax・・・�@
を考えた時、
y=ax+t・・・�A
をとると、
t > 0の時、�@ < �A
t < 0の時、�@ > �A
t = 0の時、�@ = �A
となり、任意のtを与える事で
ax < ax+t
及び
ax > ax+t
となる(y=ax上でない)2つの領域に分けられる

で、いいんじゃないかな。
x=s
を考えた場合は、同様にx=tを取り、
t > s, t < s, t = s
で考える。

y=sの時も同様。

平面上の媚びた美少女は、人間ををオタと非オタに分ける

>>38
つ【座布団】

これって証明が正しいことを プ ロ グ ラ ム で 検 証 してみたってことでしょ

こういう自明と思われる事まで証明するとは・・
うーん、奥が深いな。数学って。

絶対神：医学　法学　理論経済学　美学　歴史学　
ーーーーーーーー特権階級の壁ーーーーーーーーー
超最高神：数学　哲学　神学　形而上学　抽象的
ーーーーーーーーメタ・超越の壁ーーーーーーーーー
脱最高神：理論物理学←形而下学ｗ　具体的
ーーーーーーーーー真理の壁ーーーーーーーーーー
最高神：最高裁判事　主要官庁次官　皇族　
一等神：財務・経済産業・総務省　日本の心臓部
二等神：浅田彰　批評空間　天才　米国大統領ｗ
ーーーーーーーーー聖域の壁ーーーーーーーーーー
三等神：文部科学省　神一人で皇帝１０人を支配
四等神：厚生労働省　主に医学部教授で構成
ーーーーーーーーー権力の壁ーーーーーーーーーー
皇帝：物理学者　相対的な権力者
大臣：数学者　皇帝のブレーンとして不可欠な存在
貴族：宇宙物理学者　地球物理　皇帝の血族
ーーーーーーーー支配階級の壁ーーーーーーーーー
大商人：Bill Gates 　Google 　Warren E. Buffett
ーーーーーーーーー富裕層の壁ーーーーーーーーー
商：生物学者　地位は低いが景気（流行）もあって
　　　　　　　結構いい思いをしている
ーーーーーーーー人気・好感度の壁ーーーーーーーー
工：地鉱学者　影が薄い
農：化学者　実際一番圧力が厳しく貧しい暮らしをしている。
ーーーーーーーーー人間の壁ーーーーーーーーーー
奴隷：ゴミ講究　被差別階級。大臣が直々に管理。
ーーーーーーーー生存不能の壁ーーーーーーーー
飽食：博士崩れ　元は支配階級だったものの没落。
　　　稀に復活する者もいるが大半は野垂れ死に。
ーーーーーーーーーバカの壁ーーーーーーーーー
その他：どうしようもないｗ

どこに証明あるんだよ

証明したんじゃなくて証明を検証するプログラムを作ったんでしょ

証明したんだよ。何処読んでんだ

公理としては何を持ってきて、証明しないといけないのかな？

(´・ω・)　完全証明できたんだ・・・なんか、感動だ・・・

http://e-learn.mine.nu/mizar/jordancurve.htm
証明ってのはこれの下の方にあるリンクのやつか？

やはり、奴か

>>45
証明は100年前からされている.
その証明をコンピュータが理解できるようにMizer言語に翻訳しただけ.

>>50
ちゃんと中村教授のホームページ見た？
今までのは全て不完全な証明、こんどのが初の完全証明。
ミザールは、論理に循環や矛盾や不整合が無いか検出してくれるプログラムだが、
人に代わって論理を組み立ててくれる訳じゃない。
証明の論理そのものを構築して行くのは人間なの。
だから十数人もの数学者チームが14年もかかってる。
基本くらい押えてから書け。

>>51
今回の"証明"は、単にMIZARによって、証明に直観が入り込んでいる
可能性を排した、という意味で初めて完璧な証明の"検証"が出来た、ということ
それを本人が不遜にも"完全証明"と呼んでいるだけ
だから平地助教授は、完全証明がどうの、とか言わないでお茶を濁してるだろ？

位相空間論の概念を用いた厳密な証明自体は大昔から与えられていて、
一般化（アレキサンダーの双対定理）もなされているが、
計算機が検証可能な形で書き下すのは、原理的には可能だったにせよ、行われていなかった
それを公理からヒタスラ緻密に書き下すのに10年以上もかかった、ただそれだけ
もう少し事情を理解してから書き込んだらどうかな

　　　　　　　　 　 _　-‐…ｰ -　、
　　　　　　 　 ／　 　 　 　 　 　 ＼
　　 　 　 　 /　　　, 　 　 j ,ﾊ 　 　 ヽ
　　　　　　,'　!　　r{　__／l/　l,ﾊ　　　}
　 　 　 　 ｉ　l　　 !,ﾝﾁ ､｀　　_,ZV ノi′
　　　　 　 l　ﾄ､　 '、 ゝ′　　 し冫 ,'
　　　　　　ヽゝヽ,_ ＼　　 __`　ノ　/　　ばーさんは用済み
　 　 　 　 　 ＼　ヾ｀ 　 　 　 ／ ,′
　　　　　　　　　ヽト!j `' ｰ i´ '＾´
　　　　　　　　　　／l　 　 ﾉ' ＼
　　　　　　　　 ィ´　,＞＜_　　ノ,ゝ､
　　 　 　 　 /　/ｰｆく.ｲﾄ､> ﾌ´ �h　ヽ
　　　　　　 ｉ　 ｌ 　 `‐ｌ ｌ‐ '′　､ｌ　　 ',
　　　　 　 /　 ｌ　 　 ｜|　　　　ﾉ　　　 i
　　　　　　ゝ-ｌ　　　◯◯　　　ヽ-‐ ‐〈
　　　　　　i￣!　　　　　　　　 　 `｢￣ !
　　　　　 ,'　 !　　　　　　　　　　　l　　 !
　　 　 　 !　r' ┐　　　　　　i' ´￣ l　　 !
　　　　　ｌ　ゝ.ノ　　　　　 　 ヽ-- ‐l　　 ',
　　　　　!　!　　　　　　　　　　　 　 ',　　 ',

これだけの手間を掛けて、検証したことには驚きを感じる。

ルドルフの業績を評価する派、しない派
そんな事議論しても面白くないなぁ

証明はよくわからんけど直感でそうだと思っていたオレは天才かな

日の丸がどんな形になろうとも、白地と赤字には境界がある・・ってあたりまえでしょで終わってしまうなぁ、俺。

どんな闇の世界にだって抜け道はあるもんだ。

>52
お前どうしようもないやつだな

証明に使用した他の基礎概念が知りたいんだが。

平面状の２点間に引ける線はある、とかそんな概念すらなかったら大変だしな。

要するに、理学（数学）ではなく工学（情報科学？）の仕事
ペンローズも言ってるとおり、情報科学は既にある情報を加工する
のが仕事だが、数学は人間の頭の中で情報を創造する仕事だ。

1. 単位円は平面を内側(x^2+y^2＜1)と外側(＞1)に分ける。
2. 閉じた曲線は単位円と同相。
3. ゆえに、閉じた曲線は平面を内側と外側に分ける。

自明に思えるんだが、欠陥はどこ？
1は数論的にどうしようもなく明らかなんで、2か3が怪しいのか？

情報を創造するなんておこがましい｡

数学は彫刻と同じだ｡
表面上は何もない木片の奥に静かに隠れている、アートを
注意深く取り出す作業だ｡

彫刻家は、ノミとハンマーを使って
数学者は、ペンとコンピューターを使って。

すまそ，誰かこの証明をする為に使った公理を教えて

>>62
どう考えても証明しないといけないのは 1. でしょ．
外側とか内側って何？ってことじゃないの．
数論って何よ？w

証明に成功したのか、
証明が正しい事を証明する事に成功したのか
どっち？

Mizerが理解できるように証明を補って, Mizerに証明を検証させた.

数学の言葉を論理学の言葉で解釈しなおして, 検証させた.

>>62
同相写像は、曲線はともかく平面の残りには、どう働くんだ？

そういえばﾎﾟｱﾝｶﾚの定理はどうなった？
確か証明出来たんだよな？

折れ線なら数ページでできますよ。

>69
ニューススレは前にどっかあったけど、中身は80％がカレーの話だったよ。

62歳か、退官直前なのに凄いな