トップページ⇒math
1001コメント361KB

ジョルダンの曲線定理が完全証明される

■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん2005/09/28(水) 02:15:26
★ジョルダン：曲線定理、世界初の完全証明　信州大教授ら

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

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

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

　http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html
0002１３２人目の素数さん2005/09/28(水) 02:20:12
「私達が始めて完全証明した」とはおこがましい
ヘボい企業の人が営業で言いそうな台詞だ。
0003１３２人目の素数さん2005/09/28(水) 02:27:12
コムのチェック機能かぅ
0004１３２人目の素数さん2005/09/28(水) 02:47:44
プルーフチェッカーのデモの一つとして、曲線定理をやってみただけでは？
0005１３２人目の素数さん2005/09/28(水) 02:49:57
今井数学的だな
0006１３２人目の素数さん2005/09/28(水) 02:56:29
ニュー速よか盛り上がりが低い、ってのもねえ。
0007１３２人目の素数さん2005/09/28(水) 02:59:59
ニュー速+
【研究】「実社会にも応用可」 "ジョルダンの曲線定理"、世界初の完全証明…信州大教授ら
ttp://news19.2ch.net/test/read.cgi/newsplus/1127835258/
0008１３２人目の素数さん2005/09/28(水) 03:00:57
その２０万行を全部見ないことには何とも

もっともそんなの見る気にもならんが
0009１３２人目の素数さん2005/09/28(水) 03:16:29
>>4
たぶん、それが「証明」じゃなくて「完全証明」の意味だろうね。
中村さんのサイト

ttp://e-learn.mine.nu/mizar/jordancurve.htm

には、最初に証明したのは「Oswald Vebren」と書いてあるけど、
「Veblen」のミススペルだから、ここ見てたら直してね。
0010１３２人目の素数さん2005/09/28(水) 07:36:34
>>8
ftp://mizar.uwb.edu.pl/pub/version/mml/jordan.miz
ftp://mizar.uwb.edu.pl/pub/version/abstr/jordan.abs

http://e-learn.mine.nu/mizar/jordancurve.htm に
>Oswald Vebren が　1905年に一応の証明をしたと言われていますが、前提
>となる知識の到るところに直感が使われ、完全証明とは言いがたいものでした。
とあるけど、「直感が使われ」ていたのは具体的に証明のどの部分なのだろう？
0011１３２人目の素数さん2005/09/28(水) 07:51:59
20万行…
証明の長さ的にもギネス級でわ？
0012１３２人目の素数さん2005/09/28(水) 07:55:41
20万行…
ごジョルダンでしょ？
0013１３２人目の素数さん2005/09/28(水) 08:15:43
>>10 公理からダイレクトに出してない，くらいの意味だとおも
0014１３２人目の素数さん2005/09/28(水) 09:11:46
これは下手をすると

「数学者は役たたず．自分の縄張りの問題も解決できない
やっぱり工学は偉い」

みたいなレトリックに転嫁されそうですね

数学プロパのみなさん
曲線定理の経緯とこの信州大の人の仕事の意義を
詳しく説明してください
0015１３２人目の素数さん2005/09/28(水) 09:56:41
・ この信州大の人の仕事の意義
4 名前：１３２人目の素数さん[] 投稿日：2005/09/28(水) 02:47:44
プルーフチェッカーのデモの一つとして、曲線定理をやってみただけでは？

・ 曲線定理の経緯と
10 名前：１３２人目の素数さん[sage] 投稿日：2005/09/28(水) 07:36:34
>Oswald Vebren が　1905年に一応の証明をしたと言われていますが、前提
>となる知識の到るところに直感が使われ、完全証明とは言いがたいものでした。
とあるけど、「直感が使われ」ていたのは具体的に証明のどの部分なのだろう？
13 名前：１３２人目の素数さん[sage] 投稿日：2005/09/28(水) 08:15:43
>>10 公理からダイレクトに出してない，くらいの意味だとおも
0016１３２人目の素数さん2005/09/28(水) 09:58:42
>>15
もうちょっとツッコんだ分析をお願いします
0017１３２人目の素数さん2005/09/28(水) 10:25:48
ミザール言語というのを、証明を記述する方式としてアピール
できたのが最大の成果ではないかな。ミザール言語からTeXへ、
TeXからミザール言語へ変換するようなスクリプトやエディタ
があると、今後は普及していくかも知らん。
0018１３２人目の素数さん2005/09/28(水) 10:33:41
プルーフチェッカーによる証明のチェックが初めて出来た、ということ

出来てない、というか、してない有名定理は五萬とある訳で

プルーフチェックが今後、簡便化されていけば、将来的に実用もあるん
じゃないかねえ？自分で書いた証明をチェッカーに掛けて検証するとか
0019１３２人目の素数さん2005/09/28(水) 10:52:22
将来的には本当の未解決問題に
自動証明を応用することはありえるのでしょうか？
0020１３２人目の素数さん2005/09/28(水) 10:56:33
>>19
当分はないんじゃない？これは既にある証明の構文チェックをするものなので、
証明をするのとは次元が違うとおもわれ。教科書の証明をどんどんミザール言語に
翻訳したり、ライブラリを作ったりするのが今後の発展方向では？

0021１３２人目の素数さん2005/09/28(水) 10:58:08
将棋とかチェスのプログラムみたいな方法論で
未解決問題を証明することはできないでしょうか？
0022のりお2005/09/28(水) 11:11:20
「完全証明」って、じゃあ俺の知ってる証明はなんなんだ？

0023１３２人目の素数さん2005/09/28(水) 11:12:22
>>21
既に自動証明と言うジャンルはある。任意の命題を一階述語論理の範囲で
真か偽か判定するものなので、その過程は証明であると言えば言える。
しかしその種のプログラムは一般に、有限時間の範囲で真または偽という
判定がでるとは限らない。囲碁や将棋では、この手は損だと思ったら
適当な基準で考えるのを止めていいんだが、証明はそうでないという
点が最も異なる。とはいえ未解決問題や証明のギャップを、有限時間
考えてみるというプログラムが登場してくる可能性はありうる。
それだって、（ミザール言語による）数式のライブラリがある程度
充実していないとなかなか機能しないと考えられるが。
0024１３２人目の素数さん2005/09/28(水) 11:16:27
だいたいわかったがミザール言語ってなんだ

これか？
http://pya.cc/pyaimg/pimg.php?imgid=18276
0025１３２人目の素数さん2005/09/28(水) 11:23:36
>>22
「厳密さは時代の関数」と言った偉い数学者がいたと思ったよ。
完全証明と言うのは、完全に厳密な証明のことであろう。気にスンナ。

>>24
Mizar言語の概要
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch2.htm
0026１３２人目の素数さん2005/09/28(水) 11:27:43
289 ：１３２人目の素数さん ：2005/09/28(水) 11:18:08
>>287
黒木のように、直観力がなく、客観に頼ろうとする人間には
数学は無理だったんだよ。結局
0027１３２人目の素数さん2005/09/28(水) 11:32:48
その前に(何の前かはおいといて)、ジョルダンの曲線定理のまともな証明
が載ってる本教えて。なるべく手に入りやすいのが有難い
0028１３２人目の素数さん2005/09/28(水) 11:35:14
>>27
Jordan, Cours d'Analyze de l'Ecole Polytechnique (1887)
0029１３２人目の素数さん2005/09/28(水) 11:40:20
クゼ･コスニオフスキ
トポロジー入門
0030１３２人目の素数さん2005/09/28(水) 13:51:59
287 ：１３２人目の素数さん ：2005/09/28(水) 11:16:27
夫馬です。

「客観的な証明は２０万行」も掛かるんだってさ。こんなの
やってられないよね。普通の証明は、「直感」的なんだよね。
客観的ではないのよ。分かりましたか
0031１３２人目の素数さん2005/09/28(水) 14:49:53
＞プルーフチェックが今後、簡便化されていけば、
＞将来的に実用もあるんじゃないかねえ？

そのためには、人間にとっては直観的に明らかな命題を
自動証明する"行間を埋める"機能が必要だね。
0032１３２人目の素数さん2005/09/28(水) 15:29:18
行間を埋める機能で足りない場合に、人間が教えてやらなければならない。
約１４年間にわたる共同作業の大部分は、人間にとって間を埋められるのが
わかりきっている部分を、計算機に手取り足取り教えるのに費されたのでは
ないかと。
0033１３２人目の素数さん2005/09/28(水) 15:41:29
＞わかりきっている部分を、計算機に手取り足取り教える

もし黒木が査読者だったら、んなことせにゃならんのか？
0034１３２人目の素数さん2005/09/28(水) 15:44:01
これからの数学論文はミザール言語で書く必要がありますね
0035１３２人目の素数さん2005/09/28(水) 15:44:27
>>28
それは最初にクレームしただけで、間違っている。Veblen の1905年論文は
ぐぐるとヒットするはず。シェーンフリース1906やL.ブラウワ1909（不動点定理
のほう、有限群のほうはR.ブラウワ）の論文もある。

Jordanよりも四色問題やケプラー問題のプルーフチェックをしてくれると
助かるね。
0036１３２人目の素数さん2005/09/28(水) 15:45:59
>>32
って事は結局、自動証明が実用的なものにならない限り、
人手も時間も掛かりすぎて駄目っぽいな
0037１３２人目の素数さん2005/09/28(水) 15:51:18
>>36
通常、「自動証明」というのは人間にとっても意味のある定理を
証明することを目標にする

この場合は、人間にとって自明な命題を証明できればいい

厳密には区別できないが、そいうことだ
0038１３２人目の素数さん2005/09/28(水) 15:56:19
人間にとっても意味のある定理の自動証明

人間にとっては自明な命題の自動証明

この間にある間隙はいかほどのものだろう
0039１３２人目の素数さん2005/09/28(水) 16:01:17
>>37
「人間にとって自明」ってのは、「良く知られた事実」と「良く知られた論法」の中から
「その場面において適切なものを選び出」せば、わずかな手順で証明が探索出来るって事だよね。
数学的事実とか論法のデータベース化と、
それらをどんな場面でどうやって組み合わせるのが適切か、という知識のデータベース化が進めば、
人間にとって自明な命題が証明出来るようになるのかな。
0040１３２人目の素数さん2005/09/28(水) 16:04:10
Mizarはproof checkerだから、自動証明とは関係ないね。
既存の証明をMizar言語に翻訳して、Mizarに食わせて、
受理されるかどうかを確かめるってハナシでしょ。

しろうとの勘違いだったらスマン。
0041１３２人目の素数さん2005/09/28(水) 16:06:54
＞既存の証明をMizar言語に翻訳して、Mizarに食わせて、
＞受理されるかどうかを確かめる
それで済むなら、既に実用段階に近いということだね。

どっちが正しいのかは知らないが
0042１３２人目の素数さん2005/09/28(水) 16:07:44
自動証明なんて出来ないから考えてもムダ。
それより、表題の件は証明チェッカーを通すために人間が
証明を機械にわかる形に書いたのが２０万行ってことだろうな。
このステップ数をなんとか数千行くらいまで落とせれば実用になるだろう。
0043１３２人目の素数さん2005/09/28(水) 16:09:50
Mizarの概要

このプロジェクトの目的は数学の論文のチェックのシステムを作ることです．
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch1.htm
0044１３２人目の素数さん2005/09/28(水) 16:11:34
「人間が書いた証明が２０万行」かよ。こりゃ、たまらんな
0045１３２人目の素数さん2005/09/28(水) 16:13:51
「人間が書いた２０万行の証明」を「Mizarプルーフチェッカー」に
食わせた、ということか？
0046１３２人目の素数さん2005/09/28(水) 16:21:28
＞Oswald Veblen が　1905年に一応の証明をしたと言われて
＞いますが、前提となる知識の到るところに直感が使われ、
＞完全証明とは言いがたいものでした。
数学の定理のほとんどは、そうなのだが…

直感なしの証明が与えられている定理なんて、ほとんどない
0047The_Knight_of_Mathematics ◆uGlSZOV4Kc 2005/09/28(水) 16:23:11
････････････（20万行）
････････････････････････････････････････････
････････････････････････････････････････････
････････････････････････････････････････････
････････････

これが証明すべきものであった．
0048１３２人目の素数さん2005/09/28(水) 16:26:15
もしも人間が２０万行も書かなければならないのだとしたら、
実用には耐えられないわな。せめて１千行〜１万行でないと。

＞このプロジェクトの目的は数学の論文のチェックのシステムを作ることです．
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch1.htm
0049１３２人目の素数さん2005/09/28(水) 16:29:22
結局、「人間が書いた１千行の証明」を「２０万行の完全証明」に
自動変換するシステムが必要になるな。
0050The_Knight_of_Mathematics ◆uGlSZOV4Kc 2005/09/28(水) 16:29:39
>>48
そのためにPDが職を得るのSA
教授の原案をもとに数十人がかりでNA
世の中うまくまわるようになっるYO
0051１３２人目の素数さん2005/09/28(水) 16:30:37
程度問題だろう。自然数の概念だって直感がないと理解出来ないし。
だからって、その概念があいまいで信用出来ないってことはない。
ある意味、直感ほど正確で信用おけるものはない。
程度によるけど。だから程度問題。
0052１３２人目の素数さん2005/09/28(水) 16:30:38
>>49
自動証明はやったのか？やらなかったのか？それが問題だ！
0053１３２人目の素数さん2005/09/28(水) 16:32:21
>>51は>>46に向けたもの。レスが早過ぎる
0054The_Knight_of_Mathematics ◆uGlSZOV4Kc 2005/09/28(水) 16:34:44
レズが早熟すぎる
0055１３２人目の素数さん2005/09/28(水) 16:34:56
人間にとっても意味のある定理の自動証明

人間にとっては自明な命題の自動証明

この間にある間隙はいかほどのものだろう
0056１３２人目の素数さん2005/09/28(水) 16:37:08
「人間にとって自明な命題の自動証明」ができることが
実用化の必要十分条件
0057The_Knight_of_Mathematics ◆uGlSZOV4Kc 2005/09/28(水) 16:38:26
人間の手で証明することは最上である
MIZARによるものはその次によい

- ウィリアム・メークピース・サッカリ（イギリスの小説家）
0058１３２人目の素数さん2005/09/28(水) 16:40:56
「ピタゴラスの定理」の完全証明って、何行くらいになるの？
0059１３２人目の素数さん2005/09/28(水) 16:50:01
16人の共同研究じゃ誰にアーベル賞をあげるのか迷うだろうな。
0060１３２人目の素数さん2005/09/28(水) 17:15:23
>>58
ユークリッド幾何をMIZARが食えるように書き直すってのは
まあ面白いかもね。

今回は、ジョルダンという「自明のようだが証明はわかりにくい」定理の
プルーフチェックを計算機で行ったという着眼点がよかった。

ピタゴラスの定理だったら、さほど評価されないね。
四色問題なら14年ですまないｗ
フェルマーは人間がチェックするほうがはるかに早い。

論文の TeX ソースを MIZAR に変換する自動プログラムなんて、
当分無理だしね。
0061１３２人目の素数さん2005/09/28(水) 17:26:46
>>56
だろうな。検証対象の証明文を書くにしてもライブラリに登録する文章を書くにしても、
完全に行間を埋めなきゃいけなかったら、大変すぎて非実用的。
自明な行間くらいはコンピュータが自分で補ってくれないと。
「組み合わせ的に考察すれば明らか」とか「定数項に着目すれば明らか」とかを
詳しく書いてられない。
0062１３２人目の素数さん2005/09/28(水) 17:31:06
自動証明は無理だって。あきらめな
0063１３２人目の素数さん2005/09/28(水) 17:33:40
関連スレ

コンピューターによる定理の自動証明
http://science4.2ch.net/test/read.cgi/math/1126017312/
0064１３２人目の素数さん2005/09/28(水) 17:36:39
つーか、ジュルダンの定理は前から証明されているだろ。
フェルマー予想もな。

で、ほとんどの証明されてる定理には、まだ完全証明は
与えられていない。

ここ２００年の間の数学的成果で完全証明の与えられて
いる定理の割合は１％も行かないんじゃない
0065１３２人目の素数さん2005/09/28(水) 17:38:01
証明と完全証明はまったく違うものだ

完全証明⊂証明だろうけど
0066１３２人目の素数さん2005/09/28(水) 17:39:14
>>62
それはproof checkerが実用的な(人手も時間も
掛からない)ものになる可能性を否定するも同然かと。
0067１３２人目の素数さん2005/09/28(水) 17:39:25
「人間にとって自明な命題の自動証明」ができない限り
プルーフチェックの実用化は無理だよん。諦めなｗｗｗ
0068１３２人目の素数さん2005/09/28(水) 17:40:28
自動証明⊂完全証明⊂証明
0069１３２人目の素数さん2005/09/28(水) 17:47:33
>>66

proof checkerと自動証明はまったく別ものだろう。
難度から言ったら自動証明のほうがはるかに、というより可能と
不可能の違い。
0070１３２人目の素数さん2005/09/28(水) 17:52:01
>>69
proof checker の実用化＝自明な命題の自動証明
自動証明＝意味の有る定理の自動証明

という意味でなら、違うなあ
0071１３２人目の素数さん2005/09/28(水) 17:53:54
>>69
つまり、自明な命題の自動証明は可能、
意味の有る定理の自動証明は不可能と
いうことですかい
0072１３２人目の素数さん2005/09/28(水) 17:56:32
永田・可換体論の「自明」を自動証明できるレベルじゃなきゃダメだろｗ
0073１３２人目の素数さん2005/09/28(水) 17:57:28
コンピュータが自動で行間を埋めない限りは、
人間がすべての行間を埋めなければならない

それは人間が「定理の証明図」を書かないと
いけない、というのと同じ

これでは、プルーフチェックは全く実用的で
ない
0074１３２人目の素数さん2005/09/28(水) 18:00:21
>>72
「禿 藁 to appear 論文」の自明を
自動証明ができるレベルじゃなきゃ
ダメだろｗ
0075１３２人目の素数さん2005/09/28(水) 18:02:52
>>74
それが出来たら、禿ちゃんの数学者としての名誉も完全回復だね♪
0076１３２人目の素数さん2005/09/28(水) 18:04:37
>>74
それは「自明」ではなく「間違い」。百歩譲って「ギャップ」。
本人による手動証明もできるレベルでないｗｗｗ
0077１３２人目の素数さん2005/09/28(水) 18:05:26
>>75
禿ちゃん、病院のベッドの上でMIZARを必死に勉強中らすい
0078１３２人目の素数さん2005/09/28(水) 18:07:35
>>76
いや、Ann. Math. の査読者が間違っているんだよ。
正しいのは分科会だった、ということまで自動的に
証明できるよ♪
0079１３２人目の素数さん2005/09/28(水) 18:08:53
細かい行間についてはコンピュータに自分で埋めて貰って、
一定時間内に埋められなかった行間は自己申告して人間に埋めて貰う。
んでその埋められなかった行間が多すぎなければ実用的と言えるかと。

>>74-78
巣に帰れ。他スレにまで迷惑掛けるな。
0080１３２人目の素数さん2005/09/28(水) 18:10:28
>>79
そうでしょうなあ。
0081１３２人目の素数さん2005/09/28(水) 18:13:37
完全証明って何？人間の脳よりコンピューターの方が正確ってこと？
0082１３２人目の素数さん2005/09/28(水) 18:15:57
>>79
ただ、今回のは「行間を埋める」じゃなくて、何が仮定されてるのか
よくわからんから証明をチェックしてみました〜って話だから、
「自明をコンピュータで埋める」とは違うかと。

論文の自明は「ルーティンだけどめんどくさい」が多いので、
さまざまなルーティンを全部プログラムにぶち込むのは今のところは
不可能。今回は、ジョルダンに特化してるわけで、何にでも使える
わけではない。
0083１３２人目の素数さん2005/09/28(水) 18:16:32
>>81
数学基礎論（とくに証明論）の初歩の初歩をどうぞ
0084１３２人目の素数さん2005/09/28(水) 18:20:21
Mizarの概要

このプロジェクトの目的は数学の論文のチェックのシステムを作ることです．
http://markun.cs.shinshu-u.ac.jp/kiso/projects/proofchecker/mizar/Mizar-J/Miz-ch1.htm
0085１３２人目の素数さん2005/09/28(水) 18:42:27
>>83
「完全証明は史上初」という売り文句は素人相手に有効だよね。
完全証明ということばで、今までの証明は数学的に不十分だったと
思わせられるから。
0086１３２人目の素数さん2005/09/28(水) 18:49:07
>>85
そうすると、現在までに証明されているほとんどの定理には
数学的に完全な証明はないことになるんだけどね。
0087１３２人目の素数さん2005/09/28(水) 19:18:04
スレタイみて思い出したんだけど昔幾何系のスレでジョルダンの閉曲線定理を
S_nのアレキサンダー双対とかいうので証明したスレがあったとおもうんだけど
あれどこだっけ？おぼえてるひといまつ？
0088海援隊2005/09/28(水) 19:22:08
ジョルダンなんかでジョルダン言うか!
0089１３２人目の素数さん2005/09/28(水) 19:35:08
武田鉄也の弟の名前は？
0090１３２人目の素数さん2005/09/28(水) 19:48:00
Mizar言語の職人が量産されて、それがMizarドカタ等と蔑まれる時代が来るのだろうか…
0091GiantLeaves ◆zkraGArAss 2005/09/28(水) 19:53:49
>>90 それが崩れの生きる道。数学の就職問題が解決されるかも
0092１３２人目の素数さん2005/09/28(水) 19:57:14
これで中村教授も日本を代表する数学者の仲間入りか。
0093１３２人目の素数さん2005/09/28(水) 20:27:55
信濃毎日新聞のバカ記者をなんとかしてくれ!
----------------------------------------------

9月28日（水）
------------------------------------------------------------------------

ジョルダンの曲線定理　信大教授ら「完全証明」
------------------------------------------------------------------------

　信大工学部の中村八束教授（６２）＝長野市青木島、数理情報学＝が２８日
までに、約１２０年間、数学的に完全に証明されなかった「ジョルダンの曲線
定理」を、ポーランドの数学者らと共同で初めて完全証明した−と同教授が管
理するホームページ上で発表した。
　ジョルダン曲線定理は、「閉じた曲線は、平面を内と外に分ける」というも
の。１８８７年、フランスの数学者カミーユ・ジョルダンが発表した。中村教
授は「直感的には当然だが、誰も数学的に完全な証明ができなかった」として
いる。
　中村教授は１９９１年、ポーランドのワルシャワ大学ビアリストーク分校に
勤務する数学者とともに証明に取り組み始めた。同国の数学者らが管理する、
数学の証明をチェックするコンピューターシステム「ミザール」を用い、両国
の計１６人の数学者が分担、１４年かけて証明を終えた。
　中村教授は「ジョルダン曲線定理を前提にしていた多くの証明がある。今回
の証明で、そうした別の証明にも根拠を与えることができる意義は大きい」と
している。
　東工大大学院情報理工学研究科の小島定吉教授（位相幾何学）は「基本的に
は証明された定理だと考えているが、数学者にとっては、どこまで証明すれば
完全かという問題がある。ミザールを使い、完全に証明できたという点に意味
があるのではないか」としている。

0094１３２人目の素数さん2005/09/28(水) 20:30:15
ミザールを使った今回の証明が完全であることは、どう証明するの？
0095１３２人目の素数さん2005/09/28(水) 21:27:24
数学者が普通のやる厳密にしかみえない証明も
見方によっては、実はあいまいな直観にたよった証明だった
という事実に衝撃

数学側からみて物理の人の使う数学が
「いい加減なことやってんな」
と思うのに似てるのか？
0096１３２人目の素数さん2005/09/28(水) 21:49:45
>>94
互換性のある別の処理系を作って追試するしかないんじゃないか。
0097１３２人目の素数さん2005/09/28(水) 21:55:54
直感的に正しいんだからそれでいいじゃんって人はいっぱいいて。
でもそれで満足しなかった人が数学的に証明したりして。
それでも満足しなかった人が計算機にチェックさせたと。
それでもなお満足しない人はチェッカが正しいことを何らかの方法で確かめて、
その方法が正しいことを確かめて(以下無限ループ)

になるんだろうかねえ
0098１３２人目の素数さん2005/09/28(水) 21:59:48
>>97
それでも満足しない人は
公理系の妥当性を疑う

そしてノイローゼになる
0099１３２人目の素数さん2005/09/28(水) 22:23:51
＞そしてノイローゼになる
ﾜﾛｽｗｗｗ

でも実際、数学はそういう公理の元、つまりある程度人間の空想であるもの、
これの上で成り立っているものだから、
「数学的な証明」っていうのはどうなってくるんだろうなぁ。。。
0100１３２人目の素数さん2005/09/28(水) 22:38:23
>>99
人によっては、人間の存在とは全く別個に数学的現象の実在を信じ、
実在する数学的現象を人間が記述する事が数学である、と思ってる人もいる。
そういう人にとっては、公理ってのは人間が後から取ってきた一つの言語に過ぎないし、
ZFCか型の理論かそれら以外かとかもどうでもいい事。

ゼータの実在を信じてる人も。
0101992005/09/28(水) 22:49:31
>>100さん：
マジレスありがとうございます。
そういう捉え方もありましたか。。。
何か数学について人間について考えさせられました。本当にありがとうございます。

数学って物理的な部分を持つ反面、何かと哲学っぽいですね。
■ このスレッドは過去ログ倉庫に格納されています