ジョルダンの曲線定理が完全証明される
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2005/09/28(水) 02:15:26・フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの
数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との
約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が
完成。中村教授らは「完全証明したのは世界初」としている。
「ジョルダンの曲線定理」は「平面上の閉じた曲線は、平面を曲線の内と外に分ける」
というもの。直感的には明らかだが、数学的な証明は難しいとされてきた。
中村教授によると、人間が行った数学的な証明をチェックする「プルーフ・チェッカー」
というコンピューターシステムのうち、今回はポーランド・ビアリストーク大のアンジェイ・
トリブレッツ博士（６４）らが開発した「ＭＩＺＡＲ（ミザール）」と呼ばれるシステムを使用
したという。中村教授は「同様のシステムでコンピュータープログラムにミスがない
ことを確認するなど、今回の成果は実社会にも応用できる可能性がある」と話している。
http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html
0175１３２人目の素数さん
2005/09/29(木) 16:55:35そのヒルベルトの幾何学基礎論による証明かい？
すり替えはよくないね。学問を否定する悪行だよ。
0176１３２人目の素数さん
2005/09/29(木) 16:57:30いや公表はされてるんだけど
あまりに膨大で入りくんでいるため
確認がとれない
最近の Aschbaher らの仕事で
あやしかった部分が克服されて
ようやく完成したと見ていいでは(？)
という話
0177１３２人目の素数さん
2005/09/29(木) 16:59:17中村八束氏の仕事の先駆といってもよいものだ。
つまり、ヒルベルトの証明と通常の作図による証明の差を理解すれば
形式的証明と通常の証明（あるいは説明）の差を理解できるはずである。
0178１３２人目の素数さん
2005/09/29(木) 17:03:01では、公式見解の叩き台を考えましょう。
数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないか、と大きな期待を抱かせるものである。
0179１３２人目の素数さん
2005/09/29(木) 17:05:12別にそんなこと一言も主張してないが
初めて習うときに多分に直観的な証明がされて何が悪い？
0180１３２人目の素数さん
2005/09/29(木) 17:08:29数学者の間では既に証明されたと認められている定理ではあっても
形式主義的に満足できる証明がなされているものは、非常に少ない。
例えば、ワイルズによって証明がなされたフェルマーの最終予想も
形式的証明までは、まだ遠いようである。今回の中村氏らの研究は
それらの定理にも、形式的な証明が与えられるようになる第一歩と
なるのではないかと我々数学者に大きな期待を抱かせるものである。
最後の行に「我々数学者に」を入れてみたけど
0181１３２人目の素数さん
2005/09/29(木) 17:08:47計算機によって証明が検証された！とか言っても
今度は計算機とそのプログラムの信頼性の問題が出てくるわけで
往々にして健全な直観の方が信頼が置けたりするわけで
まあ、たとえJordan曲線定理にしか適用できないようなモノだったにせよ、
それまで殆ど計算機科学者の机上の空論だった証明チェッカが
初めて実際に実際の数学の定理の証明をチェックした、
という意味で意義の有る仕事だとは思うけどね
0182１３２人目の素数さん
2005/09/29(木) 17:11:47形式的証明以外はすべてただの説明である、証明に非ず
って暗に言ってるような感じで一寸違和感があるな、、
直観が混じった証明か、原理的に論理規則と公理だけからできる証明かは
数学者だったら簡単に区別くらいつけられる
0183１３２人目の素数さん
2005/09/29(木) 17:13:51だから形式証明なんかほとんどの数学者は必要としてないんだって。
手軽に出来るならケアレスミスのチェック用に便利っていうだけ。
だけど手軽になんか出来ないだろ。
0184１３２人目の素数さん
2005/09/29(木) 17:14:12＞初めて習うときに多分に直観的な証明がされて何が悪い？
問題は、その直観が隠れた前提を持っているかどうか。
例えば作図の場合、たいていの人は作図による合同と
物理的な「切った貼った」の違いに気づかない。
しかし、非ユークリッド幾何学のクラインモデルや
ポアンカレモデルを理解するにはこの違いに気づく必要がある。
0185１３２人目の素数さん
2005/09/29(木) 17:15:18＞往々にして健全な直観の方が信頼が置けたりするわけで
それは今のところね。しかも、健全な直観を獲得するのは
ごく専門領域に限ったとしても大きな労力を要することは
君もよく知っているはずだよね
だから、コンピュータによる自動化が今後なされることは、
それなりに意味のあることだろう。まだ実用段階にはない
だろうけど。特に数学の証明問題の自習に役立つと思うし、
数学者だって自分の証明のチェックに使えるだろう
0186１３２人目の素数さん
2005/09/29(木) 17:17:51「必要ない」なんていったら、角が立つだろう。
これは政治的な話でもあるんだよ。素人の誤解を
解きつつ、見解は相手を立てる言い方にしないと
0187１３２人目の素数さん
2005/09/29(木) 17:19:19新聞記者が勝手に都合の良い所だけ切り取ってきた、という可能性もあるがな
0189１３２人目の素数さん
2005/09/29(木) 17:20:25＞往々にして健全な直観の方が信頼が置けたりするわけで
プログラムのミスも人間のミス（ｗ
それも含めて人間がミスしやすいのは明らか。
>>182
そう読むのは間違っている。
＞ 直観が混じった証明か、原理的に論理規則と公理だけから
＞できる証明かは数学者だったら簡単に区別くらいつけられる
これは大嘘。数学者は無意識に直観を混入させている。
その直観が論理規則と公理で正当化できるかどうかなど
数学者にはさしたる関心はない。時間の無駄だからだ。
0190１３２人目の素数さん
2005/09/29(木) 17:21:41そんなに手軽に証明チェックが出来るようになるものかな？
普通証明する場合は同様に、で済ませるようなところだって
機械はそれじゃ理解してくれないし
0191１３２人目の素数さん
2005/09/29(木) 17:23:36当時の現実的可能性の少なさに負けたとも言える
その可能性を追求している人達を無碍に否定する
必要もなかろうて
0192１３２人目の素数さん
2005/09/29(木) 17:26:58いや、必要ないと思ってるならはっきりそういうべきだろ。
喧嘩が怖いチキンは真っ先に食われる。
0193１３２人目の素数さん
2005/09/29(木) 17:27:11＞機械はそれじゃ理解してくれないし
だから、今はね。今後の可能性を否定
しなくてもいいでしょ。そういうこと
やってる人の研究を、部外者が見解を
出すに当たっては気の利いたリップ・
サービスをしてこうぜ
２chで誹謗中傷は、大いに結構だがｗ
0194１３２人目の素数さん
2005/09/29(木) 17:29:10・オレが理解できたらその定理は正しい
（ただしオレ自身が証明した定理を除く）
0195１３２人目の素数さん
2005/09/29(木) 17:30:04やれやれ批判と誹謗中傷と区別できない馬鹿がここにもいたか。
0196１３２人目の素数さん
2005/09/29(木) 17:31:22必要ないのは、多くの数学者の感覚に過ぎないだろ。
大体、数学会には「基礎論屋」だっているんだから
基礎論屋なんて追い出せ、という教条主義を掲げる
決意をこれからは持つというならそれもありかもな
そいつらは必要だと思ってやっているわけだから、
それに合わせてやれ
0197１３２人目の素数さん
2005/09/29(木) 17:32:18・オレが理解できないのに機械が検証したなんて認めない！
0198１３２人目の素数さん
2005/09/29(木) 17:34:34>ヒルベルトは「必要」という立場だったわけでさ
根拠は？
0199１３２人目の素数さん
2005/09/29(木) 17:35:02＞それなりに意味のあることだろう。まだ実用段階にはない
＞だろうけど。特に数学の証明問題の自習に役立つと思うし、
＞数学者だって自分の証明のチェックに使えるだろう
実用化されれば、役立つじゃんか。まあ、実用化されるのに
どれだけ時間が掛かるのは分からんがなｗ
0200１３２人目の素数さん
2005/09/29(木) 17:35:31いまや、ロジシャンなんてソフトウェア科学会とか
科学哲学会あたりに亡命しちまったと思ったが（ｗ
数学屋の嫌論理なんてのはヨーロッパの反ユダヤ主義
くらい根深いもんだろ。
0201１３２人目の素数さん
2005/09/29(木) 17:36:39一般に流布している常識を知らない？まあ、
常識が正しいという確証はないわけだが…
0202１３２人目の素数さん
2005/09/29(木) 17:39:06数学屋のプラトニズムという信仰の虚妄を明らかに
するものだからだろう。
数学的プラトニズムが極右なら
論理的フォーマリズムは極左
0203１３２人目の素数さん
2005/09/29(木) 17:40:24別に基礎論屋がこういう証明を支持するかというと
また微妙かもしれないけどね
>>200
50年前にこういうふいんきは無かったはず
というか、日本特有じゃないのかな、基礎論異端視がこんなに激しいのは
0204１３２人目の素数さん
2005/09/29(木) 17:41:370205１３２人目の素数さん
2005/09/29(木) 17:42:52常識なら根拠くらい挙げられるだろう。
0206１３２人目の素数さん
2005/09/29(木) 17:44:53＞別に基礎論屋がこういう証明を支持するかというと
＞また微妙かもしれないけどね
彼らは専門家だから、より慎重でしょう。
ただ、こういう方向性の研究自体には、普通の数学者
よりも親近感を持つ人が多いでしょう。中には、近親
憎悪的過剰反応を示す香具師もいるかも試練が。
0207１３２人目の素数さん
2005/09/29(木) 17:45:07>するものだからだろう。
どう明らかにするんだよ。
0208１３２人目の素数さん
2005/09/29(木) 17:46:28「ヒルベルトは形式主義の提唱者」という常識
0209１３２人目の素数さん
2005/09/29(木) 17:47:28いや、世界的傾向だね。
ロジックは結局言葉の学問だからね。
たいていの日本人は、ロジックが存在する意味すら理解できていない。
だから、極少数の理解者は、さながら隠れキリシタンのようなもの。
0210１３２人目の素数さん
2005/09/29(木) 17:50:15どっかの研究科みたいに、教条主義を掲げて別分野をパージしますか？ｗ
0211１３２人目の素数さん
2005/09/29(木) 17:52:44『面白さ＆有用さ』にあるからね。
0212１３２人目の素数さん
2005/09/29(木) 17:53:03俺は205じゃないけども
ヒルベルトの形式主義は別に計算機で証明をチェックすれば
厳密性が確保できる、とか言うことじゃなくて
証明を形式的に書き下せば自然数論なり実数論なり、
特定の形式的数学の無矛盾性が証明できるから、（りゃ
という思想だったはず
もちろん俺はヒルベルトの後継者だ！とか自負するのは勝手だけど
一寸ヒルベルトの考えに対する勝手な憶測が入りすぎかと
0213１３２人目の素数さん
2005/09/29(木) 17:53:03ロジシャンは興味を持つだろうね。
ただ、ロジシャンは素人のようにロジックに絶対的信頼は置いてない。
だから、フォーマルだから正しいとは言わない。
彼らが興味を持つというのは、正しいかどうかよりも、どういう
フォーマリズムによってそれが証明されるのかという仕掛け。
ある意味、マニアというかヲタク的興味。
0214１３２人目の素数さん
2005/09/29(木) 17:53:48有用さ＞＞＞厳密性
基礎論屋は、死ね！
0215１３２人目の素数さん
2005/09/29(木) 17:54:48死ぬべきなのは君だと思うな
0216１３２人目の素数さん
2005/09/29(木) 17:54:51私見では置換群が鍵のように見えるんですが…
0217１３２人目の素数さん
2005/09/29(木) 17:57:39ヒルベルトがつきぬけてるのは、文字面だけ考えればイイ！
というところに気づいた点。
ただ、こういう発想は数学者にはとっても嫌われる。
美女も骸骨だけみりゃいいみたいな感じにとられるわけだ（ｗ
0218１３２人目の素数さん
2005/09/29(木) 18:00:11マツシン先生いますか？
いたら返事をしてください
0219１３２人目の素数さん
2005/09/29(木) 18:02:11計算機でチェックするとは言ってないでしょ。大体、
当時はコンピュータがなかったんだから
ヒルベルトは２段構え
１．定理の客観性を確保するために、形式体系内で証明を行う
２．当該の形式体系が少なくとも全く無意味であることを保障
するためには、（有限の立場で？）無矛盾性を確認する
２はゲーデルによって（一応の）否定を見たわけだけど、１は
なんら否定を受けていないからさ
一応、形式的に証明されれば客観的な訳で、もちろん矛盾した
体系ならば、すべての命題が正しいから意味はないけど。その
場合であったとしても正しいということ自体は客観的ではある
0220１３２人目の素数さん
2005/09/29(木) 18:02:22いまどきの集合論屋は数学者です。
彼らを、基礎論屋とかロジシャンとか呼ぶとたいてい蹴られます。
0221１３２人目の素数さん
2005/09/29(木) 18:04:19＞２．当該の形式体系が少なくとも全く無意味であることを保障
＞ するためには、（有限の立場で？）無矛盾性を確認する
すまん、書き間違えたよん。
２．当該の形式体系が少なくとも「全くの無意味」ではないことを
保障するためには、（有限の立場で？）無矛盾性を確認する。
0222The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:04:38コンピューティングによる証明を否定するゆえはない
例えば ピタゴラスの定理の証明の一つなどで辺に接続する図形を移動することで証明とする場合を
否定するようなものだ
俺ってキングとは逆に幾何学大好きだから目で見てわかる証明のほうが美しいと感じる
0223１３２人目の素数さん
2005/09/29(木) 18:09:24別に客観性なんてヒルベルトの関心にはなかった筈。
＞一応、形式的に証明されれば客観的な訳で
しかし実際には、形式的証明は激しく読みにくい。
したがって「機械は正しいといってるがオレにはチンプンカンプン」
という状況がおきる可能性大。客観的というより「無観的」といった
ほうがいい。
0224１３２人目の素数さん
2005/09/29(木) 18:12:27>１．定理の客観性を確保するために、形式体系内で証明を行う
これ普通に数学者がやってることなんじゃないの？ ただ記号論理でやらないだけで。
0225１３２人目の素数さん
2005/09/29(木) 18:12:44だから別に読まなくてもいいんだって、
それはコンピュータに読ませるための
証明なんだからさ
ユークリッド幾何を勉強するのに幾何
学基礎論を読まなくてもいいでしょ
勉強をして感覚を養うのと、正しさを
厳密に確認するのは、違う作業だって
ことはよく知ってるでしょ
0226１３２人目の素数さん
2005/09/29(木) 18:13:26いや、全然やっていない。
0227１３２人目の素数さん
2005/09/29(木) 18:16:14もっと詳しく
0228１３２人目の素数さん
2005/09/29(木) 18:16:59＞別に客観性なんてヒルベルトの関心にはなかった筈。
集合論のパラドックスに端を発して、
数学（的定理？）の正しさを保障する
方法が必要であると考えたのが、常識
として「ヒルベルトの動機」だったと
いうことになってるよ
0229The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:17:00http://image.blog.livedoor.jp/thinkdeep/imgs/3/4/341da381.jpg
図形動かして証明するほうが早いんだよ
四色問題の証明もこの証明も
これと似たようなことしてるだけだろ
数理的な証明も不可能ではないけど
複雑な命題になるにつれて
そうした証明を読み解いて理解できるやつが少なくなる
0230１３２人目の素数さん
2005/09/29(木) 18:20:42だから、フェルマーの定理だってペアノ公理系から
（その肯定も否定も）導けるか、どうかは分かって
ないよ。数学者が証明したということと公理系から
形式的に導けるということは別物なの。
これが分かってないと、中村教授の「完全証明」と
いう言葉で誤解をしてしまう素人さんの一人に入る。
0231１３２人目の素数さん
2005/09/29(木) 18:21:11＞だから別に読まなくてもいいんだって、
＞それはコンピュータに読ませるための
＞証明なんだからさ
コンピュータを信頼する根拠は？
＞ユークリッド幾何を勉強するのに
＞幾何学基礎論を読まなくてもいいでしょ
それはむしろ君の主張を否定するもののような希ガス
＞勉強をして感覚を養うのと、正しさを厳密に確認するのは、
＞違う作業だってことはよく知ってるでしょ
理解せずに正しさを確認できるという発想は
どこか精神を患っている希ガス
0232The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:23:30パズルが噛み合うから証明できたよーんっていうようなものだろ
ほら見ろよ 噛み合ってんじゃん！って
その証明を否定しようにもスパコンひっぱってこなきゃならんし
20万行読まなきゃならんしで大変･･･
今後はこういう証明が台頭する状況になっていくかと
0233１３２人目の素数さん
2005/09/29(木) 18:25:17>ペアノ公理系から
なんでペアノ公理系からなの？
集合論の公理系でいいじゃない。
そこからフェルマーは証明されてんでしょ。
0234１３２人目の素数さん
2005/09/29(木) 18:28:43ああ、いろいろ使ってるからなあ。
しかし、素人の誤解とかいう時点で
君も玄人の誤解に陥ってるな（ｗ
0235１３２人目の素数さん
2005/09/29(木) 18:30:13＞理解せずに正しさを確認できるという発想は
＞どこか精神を患っている希ガス
別に理解しなくても。「正しさだけなら確認」
できる。というのが、ヒルベルトの形式主義。
もちろん、それに対して貴方がどう思うかは、
自由だよ。
ま、単に「正しい」という言葉で意味しいてる
事が違うだけと思うが
ただ、「君の考える正しさ」は、主観的にのみ
確認できるものだと思うけど。それはプラトニ
ズムだな。もちろん、そういう立場もあるよね
0236１３２人目の素数さん
2005/09/29(木) 18:31:26＞集合論の公理系でいいじゃない。
それも分かってないけど
0237１３２人目の素数さん
2005/09/29(木) 18:33:30はあ？ それじゃ証明されてないんじゃない。
0238１３２人目の素数さん
2005/09/29(木) 18:33:39＞だからよ 例えばこういうのとか
＞http://image.blog.livedoor.jp/thinkdeep/imgs/3/4/341da381.jpg
＞図形動かして証明するほうが早いんだよ
これはどうかな？
上は、実はすごーく平べったい平行四辺形が隠れてるのが
トリックなわけだが、絵で書いても容易には見つからない。
0239The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:34:18俺にはもうついてけんよ
0240１３２人目の素数さん
2005/09/29(木) 18:36:04だから、「基礎論の初歩」を知っている数学の先生に
聞いてみな、ね
この「中村氏の完全証明」と「普通の証明」の違いが
分からないんですけど、どういうことですか？、って
結論から言えば、「普通の数学者の証明」は形式的に
証明できるということとは違うんだ、って答えになる
0241１３２人目の素数さん
2005/09/29(木) 18:40:15＞別に理解しなくても「正しさだけなら確認」できる。
＞というのが、ヒルベルトの形式主義。
違うなあ。「理解しなくても」「確認できる」なんていうのは
君が勝手にそう思ってるだけのこと。
実際には数学の理屈は文字の操作に完全に還元できるという発想。
まあ、唯名論だな。
しかしこれは大きな落とし穴がある。
つまりそもそも文字操作として表した形式化が正しいかどうかは
分からんってこと。だから実は理解ぬきには客観性なんかないって
ことさ。論理マンセーの素人が必ず陥る初歩的な穴だな。
0242１３２人目の素数さん
2005/09/29(木) 18:40:19だから、中村氏の発言になるんでしょ？
ジョルダンの曲線定理は、数学者の言う普通の意味では
証明はできていたけど、形式的証明はできていなかった。
今回、我々はそれに成功したぜ
って言っているの。
0243１３２人目の素数さん
2005/09/29(木) 18:43:05君はもしかしてワイルズの証明はどこかで
公理に拠らない直観を使用しているかもしれないから
計算機で確認するまで証明されたとは認めないつもりかな
おかしな人だなあ、というのが普通の数学の人の反応な訳だけど
0244１３２人目の素数さん
2005/09/29(木) 18:43:58たとえ証明の途中で集合論的な選択公理を援用したにせよ、
原理的には証明からそのような除去できる、って定理があったから
かなり弱い公理から導けると思って間違いないかと
0245１３２人目の素数さん
2005/09/29(木) 18:44:05いまどき、基礎論なんて古臭い言葉を繰り返す奴は
ロジックの初歩も知らんというのが相場。
こっちは、ロジシャンから聞いたこと書いてるんだよ。
0246１３２人目の素数さん
2005/09/29(木) 18:45:50>結論から言えば、「普通の数学者の証明」は形式的に
>証明できるということとは違うんだ、って答えになる
それは程度問題じゃないの。本質的違いじゃなくて。
だから今回みたいに数学者の証明を書き下していけば機械に通るわけで。
0247１３２人目の素数さん
2005/09/29(木) 18:46:08マジックの初歩も知らんというのが相場。
こっちは、マジシャンから聞いたこと書いてるんだよ。
0248１３２人目の素数さん
2005/09/29(木) 18:46:30あのねえ、普通の数学者は、原理的には時間をかければ
計算機で検証可能なレベルで、厳密に定理を証明できるだけの能力は持ってるよ
（まあ幾何学者とか一部あまり厳密で無い人も居るけど）
単に時間が無駄だからそうしないだけでね
0249１３２人目の素数さん
2005/09/29(木) 18:46:45そこは問題にしない、というのが形式主義だろ？
君がその考えは取りたくないというのは勝手だよ
しかし、それだとどこにも客観性はないが。別に
そういう立場はありだ、と思うよ。でも、それは
貴方の考えで。いろんな考え方があるの。
形式主義の考え方ならこうなるよ、って言ってる。
で、中村の完全証明っていうのは、そう言う話だ。
それに価値があるか、どうかは人それぞれの価値
観だ。俺も「ジョルダンの曲線定理の形式証明」
自体にそんなに価値がある、とは思ってないけど。
これは俺の個人的価値観だから。
0250The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 18:46:58平面上の閉じた曲線は、
↓
○
↑
平面を曲線の内と外に分ける
これが「ジョルダンの曲線定理」だっ！！！
生徒→ ('A`)「････」
0251１３２人目の素数さん
2005/09/29(木) 18:49:13激しく勘違い。もう君は駄目だ。「基礎論の初歩」を知ってる
普通の（基礎論でない）数学者に聞いてみろよ。直接
やっぱり公式見解が必要かな。こういう勘違い君がいるとこを
見ると。どうにかしてくれって感じだが
0252１３２人目の素数さん
2005/09/29(木) 18:50:23＞そこは問題にしない、というのが形式主義だろ？
重大な間違いだな。誰もそんな馬鹿げたことはいっていない。
＞しかし、それだとどこにも客観性はないが。
君が間違ってる。むしろ問題にしないほうが客観性がない。
そういう立場は君だけの主観的なものだな。他人には通用しない。
君の同類には通用するかもしれないが、具体的な事例になると
君と君の同類の見解はことごとく相違し、了解がとれなくなるだろう。
要するにコミュニケーションを否定した独我論に陥ってるわけだ。
プライドばかり強いとそういう馬鹿げたことになる。
0253１３２人目の素数さん
2005/09/29(木) 18:52:44だから、君のいう「基礎論の初歩」は間違いだよ。
まったく素人に限って勝手に自分の中に似非専門家を
つくるから困ったもんだ。素人が即座に専門家に
なれるわけがないだろ。
0254１３２人目の素数さん
2005/09/29(木) 18:55:36何だか、数学の話じゃなくなってるんですが…
何だか、君は哲学的見解を主張されてるようで
数学者は「数学者同士で」、ある程度、共通の
主観を持っているから高度な数学の話が通じる。
実際、俺はそう感じているよ
0255１３２人目の素数さん
2005/09/29(木) 18:57:41はあ？初歩なんだから、専門家じゃなくても分かっていても
可笑しくないだろ。
数学の専門家じゃなくても、数学の初歩を知ってる人はいる
よね。
0256１３２人目の素数さん
2005/09/29(木) 18:58:350257１３２人目の素数さん
2005/09/29(木) 18:59:10>>249の「そこは問題にしない」というのは数学じゃないよ。
＞数学者は「数学者同士で」、ある程度、共通の主観を
＞持っているから高度な数学の話が通じる。
＞実際、俺はそう感じているよ
共通かどうかはともかくとして、実際には数学者自身の理解と
相互の了解が、数学の定理の正しさを根拠づけているという
主張は私自身がここでしてきたことで、いまさら君の主張だと
言い張られても迷惑なんだが。
0258１３２人目の素数さん
2005/09/29(木) 19:01:22いや、初歩だから、素人が誤解しても可笑しくないんだよ。
見当違いのことをいう人は、たいてい初歩からダメだよね。
君がそう。どうせ独学だろ？だから誤解したまま気づかないんだ。
独学は結局自慰だからな。
0259１３２人目の素数さん
2005/09/29(木) 19:03:00勘違いしてるのは君だよ
俺は別に数学の普通の論文がどれくらい論理的に緻密に
書かれてるか、なんてことは主張して無い
ただ書こうと思ったら書けるよ、と言ったまでのこと
0260１３２人目の素数さん
2005/09/29(木) 19:04:04＞相互の了解が、数学の定理の正しさを根拠づけているという
＞主張は私自身がここでしてきたことで、いまさら君の主張だと
＞言い張られても迷惑なんだが。
だから、それが数学者が普通の意味で言う証明です。
それと、「形式的証明」は違いますよ、って言う話
なんだがなあ。それは分かるでしょ。
俺は、普段、形式的証明なぞ全くしないし、貴方の
定理は（かくかくしかじかの形式体系で）証明でき
ますか？と聞かれたら、「全く分かりません。どう
なんでしょう？」としか、答えようがないよ。
0261１３２人目の素数さん
2005/09/29(木) 19:05:390262１３２人目の素数さん
2005/09/29(木) 19:10:17普通はしない。それに普通の証明したからって、
それで形式的に証明できるのか、どうかなんて、
全然、分からないよ
で、今回、中村は形式的に証明できましたって
話でしょ。
もし、今までの数学者の証明＝形式的証明なら
中村の「初めて」って話は嘘になるけど、俺は
嘘だと別に思わないな
0263１３２人目の素数さん
2005/09/29(木) 19:12:30一階の述語論理が人間の推論様式を全般に渡って記述しうるというのは
十分な検証を要する一種のドグマである。」 by 某W先生
「一階の述語論理」の部分を「NBG集合論」にしてみたり、
「人間の推論様式」の部分を「数学者の推論様式」にしてみると、
＞書こうと思ったら書けるよ
ってのは楽観的すぎかなとも思う。
0264１３２人目の素数さん
2005/09/29(木) 19:14:23ホモロジーって結局何なの？
ttp://cheese.2ch.net/math/kako/1009/10092/1009270205.html
0265１３２人目の素数さん
2005/09/29(木) 19:15:40まあ初めて「形式的に証明」できました、じゃ無くて
初めて「完全証明」できました、なんて言っちゃってるけどな
>>263
まあそりゃそうだね
0266１３２人目の素数さん
2005/09/29(木) 19:19:22しかし、「形式的証明」は今回、初めて我々の手によって与えら
れましたって言うんだから
結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は
違うわけで
0267The_Knight_of_Mathematics ◆uGlSZOV4Kc
2005/09/29(木) 19:28:29ジョルダンの曲線定理とジュルダンの定理はどう違うんだ？
0268１３２人目の素数さん
2005/09/29(木) 19:32:02ジェルダンの曲線定理の「普通の証明」なら、とっくに
あった、でＦＡ。
0269１３２人目の素数さん
2005/09/29(木) 19:33:30>結局、ジュルダンの定理の「普通の証明」と「形式的な証明」は
>違うわけで
誰も同じとは思ってないだろ。
だけど、これは量の問題であって質の問題じゃないだろ。
他の証明、例えばフェルマーの定理の証明だって時間と手間を
かければ形式証明が出来るだろう。そんなことは昔からわかってることだろう。
0270１３２人目の素数さん
2005/09/29(木) 19:35:57＞ポーランドの数学者ら１６人との約１４年間にわたる共同作業
って14年間も何してたんだろ
0271１３２人目の素数さん
2005/09/29(木) 19:43:06＞かければ形式証明が出来るだろう。
その肯定が形式体系から証明できるか、どうかは
分かりません。
ただし、その手の専門家によれば、今までの経験
から予想するに証明できる公算が高いのではない
か、という噂なら聞いたよ
「時間と手間を掛ければ、形式的証明ができる」
ことが分かってるなら形式式証明ができてるのと
同じことじゃないか？
でも、少なくともジョルダンの曲線定理は、そう
じゃなかったよね。ということは「数学者の言う
証明」は「形式的証明」では必ずしもないという
ことだ。
で、ワイルズのフェルマーの定理の証明が形式的
証明だと言う根拠は何なの？
数学者が「形式的証明」であると言ってたかな？
0272１３２人目の素数さん
2005/09/29(木) 19:46:15形式的に証明できるか、どうかは分からない
よね
形式的にも証明できそうだ、という「予想」
することは何ら問題ではないけどね
0273１３２人目の素数さん
2005/09/29(木) 19:49:29＞かければ形式証明が出来るだろう。そんなことは、
＞昔からわかってることだろう。
何が分かってるの？フェルマーが証明されたのは最近。
今もまだ形式的な証明ができるかどうかは分からない。
基礎論の専門家の間では、できるのではないか？、と
予想されているという噂は聞いたよ。
0274１３２人目の素数さん
2005/09/29(木) 19:52:04誰もWilesの200ページ弱の証明がそのまま形式的証明だなんて言ってないだろ？
そんな勘違いをしてるのは君だけ
＞でも、少なくともジョルダンの曲線定理は、そうじゃなかったよね。
実際に形式的な証明が出来ただろ？
「直感的には当然だが、誰も数学的に完全な証明ができなかった」
なんていってるのは中村教授とそのお仲間だけで
平地健吾だって小島定吉だって、オリジナリティの低い低レベルな結果だ、と
内心考えてると思うよ
■ このスレッドは過去ログ倉庫に格納されています