アカウント名:
パスワード:
本家記事 [slashdot.org] (9/10) では、証明はもちろんのこと、予想自体も意味がわからんという話になっていました。http://abcathome.com/conjecture.php [abcathome.com] が理解に役立つらしいです。さらに専門の人が証明について考えるときは ここ [mathoverflow.net]が役立つらしいですが、私は一瞬で閉じました。
P=NPだとなぜ数学者が必要なくなるのかわかりません。
時間階層定理があるので、NP完全問題が自動的に解けるようになったくらいでは、数学者の仕事はなくならないよ。世の中の一般的な問題は半決定可能だし、なによりコンピュータでは未だに新しい理論を自動的に構築できないから。
数学者は証明だけでなくて予想するのも仕事で、ACから指摘されているように数学の探求世界は無限ですから仕事がなくなることはないでしょう。それに公理系そのものも数学者の研究対象ですし、P=NPなら、むしろ逆に仕事が増えるかもしれませんよ。
予想だけって、それこそ山師でもできるから（証明は計算機で時間さえあればいい）「数学者」がいまとガラッと変わることは確かじゃないかな。人間の仕事って、予想とか枠組み構築とか創造的で仕事っぽい仕事は、それだけでは仕事として成り立たず、地道な作業と結びついた「手仕事」と抱き合わせじゃないとダメなんだと思う。
数学でいう「予想」は日常会話で言うような意味では全くないので、山師にはできませんよ。予想も枠組み構築も、地道な手作業の最たるものです。
> 数学者が絶滅することはありません。数学者全員首って言ったのはお前だろうが。サラっとなかったことにしてねーでちゃんと撤回しろよ。
競輪が盛んだった某高校では、もっともらしい理屈をつけた「山田の予想」が当たると「山田の定理」に昇格していた
現代数学をかなり高度なところまで理解している山師って、意外に多いよ。コンサルとかに。あの正しくないものを正しく見せるあてずっぽうは、あなどれんと思うがな。証明がある意味手軽になった後の予想が、どの辺が地道な作業なのか、教えて。
んじゃ、反基礎集合論(AFA) と整礎集合論(FA)のどちらが「自然な数学」に相応しい公理系なのか、予想してよ。いくら証明が自動化されて作業に考えなくてもいいと言ったって、サルがシェークスピアを書く確率は0ではないですよ、と言ってるだけでしかないよ。
> 数学者が絶滅することはありません。 数学者全員首って言ったのはお前だろうが。サラっとなかったことにしてねーでちゃんと撤回しろよ。
そうですね。すみません。かなり極端でしたね。願望が入ってました。 今の数学者の9割が首になるのであれば私としては満足です。
ここまで書いてくれりゃ、俺はさる以下だが予想できる。FAが自然な数学に相応しい。AFAもFAも自然な数学も相応しいも全部定義も知らないし、根拠になる証明崩れも持ってないけど。山師が1万の予想を出しても、数学として価値ある予想はほとんどないのはいいよね。でも10億個の予想を出すとちょっとは価値のあるもんが含まれているかもしれん。となると悪貨は良貨を駆逐するとか、朱に交わればで、数学者のイメージ、役割、仕事が今とガラッと変わりそうなのは確かだね。
見事に罠にかかったみたいだけど、出来過ぎなくらいの墓穴を掘ってくれてうれしいね。その通り「ここまで書いてくれ」なきゃ要するに予想はできないんだよ。見たことも聞いたこともない知らない言葉というのはその人にとって存在しないのと同じ、存在しないものを使って何か作ることはできない。既に作られた定理を証明できることは、誰も知らない新しい言葉や道具を作れることを意味しない。存在すら知らないような言葉で書かれる「予想」の文章は、その言葉の存在すら知らない人には書けないからだ。数学者の仕事ってのは、もともとそっちの方が主なので、数学者の価値は落ちない。証明に価値がなくなるとすれば、プロブレムソルバー一辺倒でやってきてる人は多少困るだろうけどね。
もともと考えてた返答は、FAもAFAも無矛盾で、その上で大抵の数学は展開できるから、どちらが「自然」なのかは、それらの上で理論を記述する数学者の「感覚」でしかなく、それぞれ数学者の感覚はどれも正しく無矛盾に鼎立していることであって、定理証明器だけ残して数学者を殺してしまったら、何も残らない。くらいのことだったが、あなたが間抜けすぎでよかった。
> こちらで述べましたが、自動定理証明 [wikimedia.org]は正しい予想の場合NP完全問題 [wikimedia.org]だからです。リンク先には命題論理の自動定理証明はNP完全問題としか書かれてねーじゃん。一階述語論理という言葉の意味すら理解できなかったの? あまりにもひどすぎる。お前はもう定理の自動証明について一切語るな。
そもそも数学のもっとも重要な側面は、与えられた問題を解くことではありませんよ？面白い理論（公理系）を構築すること、そしてその公理系の中で面白い問題を提示することです。
証明が自動化されても定理を生み出す仕事は残るよ。
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
一つのことを行い、またそれをうまくやるプログラムを書け -- Malcolm Douglas McIlroy
oldnews (スコア:2)
本家記事 [slashdot.org] (9/10) では、証明はもちろんのこと、予想自体も意味がわからんという話になっていました。
http://abcathome.com/conjecture.php [abcathome.com] が理解に役立つらしいです。
さらに専門の人が証明について考えるときは ここ [mathoverflow.net]が役立つらしいですが、私は一瞬で閉じました。
Re: (スコア:0)
数学者の証明なんてのは人間の読むものじゃないです。
汎用的な自動証明検証が普及して、我々一般人が証明の正しさとか流れを簡単に判断できるようになればいいですのにね。
P=NPが証明されて数学者全員首が最も望ましいシナリオですけど。
Re: (スコア:0)
P=NPだとなぜ数学者が必要なくなるのかわかりません。
Re:oldnews (スコア:1, 参考になる)
NP完全問題はNP問題に含まれるのでP=NPが証明された場合、そのアルゴリズムからP問題として解けます。
P問題はたいてい解けるでしょうから、つまり証明問題は数学者の仕事でなくなるからです。
それでも数学者の仕事は多少残るでしょうが、まぁ首で差し支えありません。
Re: (スコア:0)
時間階層定理があるので、NP完全問題が自動的に解けるようになったくらいでは、数学者の仕事はなくならないよ。
世の中の一般的な問題は半決定可能だし、なによりコンピュータでは未だに新しい理論を自動的に構築できないから。
Re: (スコア:0)
今は論理ゲートでCPUを作り上げる人も、アセンブリで大きなプログラムを書く人も、円周率を手計算で何百桁求める人もほとんどいないわけですから。
世界で最も頭のいい人たちを高々計算問題にすぎない事に投入するのはもったいないです。
Re:oldnews (スコア:2)
数学者は証明だけでなくて予想するのも仕事で、
ACから指摘されているように数学の探求世界は無限ですから仕事がなくなることはないでしょう。
それに公理系そのものも数学者の研究対象ですし、P=NPなら、むしろ逆に仕事が増えるかもしれませんよ。
Re:oldnews (スコア:2)
探究分野が無限という点は、人間が手を付ける前に計算機ができるようになってしまえば構わないことです。
しかし、仕事が増えるか減るかは実際そうなってみないとわかりませんね。
C言語ができたからと言ってプログラマが居なくなったわけではありませんし。
少なくとも人間に分かりやすく有意な理論構築・予想という仕事がなくなることはないでしょうね。
小説家や買い物といった仕事が人間に残り続けるように、情報入力はいつまでも人間の役割で有り続け、またそれを十分に行うには一定の数が必要です。
最終的にそこだけに収束する事にはなるでしょうけど。数学者が絶滅することはありません。
Re: (スコア:0)
予想だけって、それこそ山師でもできるから（証明は計算機で時間さえあればいい）
「数学者」がいまとガラッと変わることは確かじゃないかな。
人間の仕事って、予想とか枠組み構築とか創造的で仕事っぽい仕事は、それだけでは
仕事として成り立たず、地道な作業と結びついた「手仕事」と抱き合わせじゃないとダメなんだと思う。
Re: (スコア:0)
数学でいう「予想」は日常会話で言うような意味では全くないので、山師にはできませんよ。予想も枠組み構築も、地道な手作業の最たるものです。
Re: (スコア:0)
> 数学者が絶滅することはありません。
数学者全員首って言ったのはお前だろうが。サラっとなかったことにしてねーでちゃんと撤回しろよ。
Re: (スコア:0)
競輪が盛んだった某高校では、もっともらしい理屈をつけた「山田の予想」が当たると「山田の定理」に昇格していた
Re: (スコア:0)
現代数学をかなり高度なところまで理解している山師って、意外に多いよ。コンサルとかに。
あの正しくないものを正しく見せるあてずっぽうは、あなどれんと思うがな。
証明がある意味手軽になった後の予想が、どの辺が地道な作業なのか、教えて。
Re: (スコア:0)
んじゃ、反基礎集合論(AFA) と整礎集合論(FA)のどちらが「自然な数学」に相応しい公理系なのか、予想してよ。いくら証明が自動化されて作業に考えなくてもいいと言ったって、サルがシェークスピアを書く確率は0ではないですよ、と言ってるだけでしかないよ。
Re:oldnews (スコア:1)
> 数学者が絶滅することはありません。 数学者全員首って言ったのはお前だろうが。サラっとなかったことにしてねーでちゃんと撤回しろよ。
そうですね。すみません。かなり極端でしたね。願望が入ってました。
今の数学者の9割が首になるのであれば私としては満足です。
Re: (スコア:0)
ここまで書いてくれりゃ、俺はさる以下だが予想できる。FAが自然な数学に相応しい。
AFAもFAも自然な数学も相応しいも全部定義も知らないし、根拠になる証明崩れも持ってないけど。
山師が1万の予想を出しても、数学として価値ある予想はほとんどないのはいいよね。
でも10億個の予想を出すとちょっとは価値のあるもんが含まれているかもしれん。
となると悪貨は良貨を駆逐するとか、朱に交わればで、数学者のイメージ、役割、
仕事が今とガラッと変わりそうなのは確かだね。
Re: (スコア:0)
見事に罠にかかったみたいだけど、出来過ぎなくらいの墓穴を掘ってくれてうれしいね。その通り「ここまで書いてくれ」なきゃ要するに予想はできないんだよ。見たことも聞いたこともない知らない言葉というのはその人にとって存在しないのと同じ、存在しないものを使って何か作ることはできない。既に作られた定理を証明できることは、誰も知らない新しい言葉や道具を作れることを意味しない。存在すら知らないような言葉で書かれる「予想」の文章は、その言葉の存在すら知らない人には書けないからだ。数学者の仕事ってのは、もともとそっちの方が主なので、数学者の価値は落ちない。証明に価値がなくなるとすれば、プロブレムソルバー一辺倒でやってきてる人は多少困るだろうけどね。
もともと考えてた返答は、FAもAFAも無矛盾で、その上で大抵の数学は展開できるから、どちらが「自然」なのかは、それらの上で理論を記述する数学者の「感覚」でしかなく、それぞれ数学者の感覚はどれも正しく無矛盾に鼎立していることであって、定理証明器だけ残して数学者を殺してしまったら、何も残らない。くらいのことだったが、あなたが間抜けすぎでよかった。
Re: (スコア:0)
> こちらで述べましたが、自動定理証明 [wikimedia.org]は正しい予想の場合NP完全問題 [wikimedia.org]だからです。
リンク先には命題論理の自動定理証明はNP完全問題としか書かれてねーじゃん。一階述語論理という言葉の意味すら理解できなかったの? あまりにもひどすぎる。お前はもう定理の自動証明について一切語るな。
Re:oldnews (スコア:1)
定義から、どのような問題でも多項式時間で自動証明検証ができる場合は(NP完全かはともかく)NP問題に当てはまります。
証明が有限長を持ち、各ステップの妥当性がアルゴリズムで検証できる場合はそうです。
少なくとも一般人が「数学」や「証明」といった場合、有効な書かれた証明を持ち、その正しさは客観的かつ一意に判定できる分野を指すでしょう。
そこに一階述語論理と書いてあるのはまさに、ゲーデルの不完全性定理から健全性かつ完全性を持つ二階述語論理にそのような条件が当てはまらないからです。
そういう分野では証明とは何ぞやすら難しい問題になりうるのです。それはどちらかといえば論理学の領域ではないですか。
数学の世界がどうなっているか余り詳しいわけではないので、普通に数学的証明と云える範囲で、多項式時間で機械的検証ができないような例があればご教授いただきたいところです。
Re: (スコア:0)
そもそも数学のもっとも重要な側面は、与えられた問題を解くことではありませんよ？
面白い理論（公理系）を構築すること、そしてその公理系の中で面白い問題を提示することです。
Re: (スコア:0)
証明が自動化されても定理を生み出す仕事は残るよ。