1 [―{}@{}@{}-] １３２人目の素数さん[sage] 2011/01/23(日) 18:18:30 .net
どうなの?
ソフトのバグだけじゃなくてハードのバグまで検証出来てるの?
2１３２人目の素数さん[sage] 2011/01/23(日) 18:21:25 .net
俺も同じこと考えたことあるけど、
それを言ったら、人間が証明読んでチェックすることの方がよっぽど信頼性低い気がする
誰か解説してくりゃれ
3 １３２人目の素数さん 2011/01/23(日) 18:47:04 .net
あくまでコンピュータで確かめただけです。
納得できないならば証明ではありません。
4 １３２人目の素数さん[sage] 2011/01/23(日) 18:51:28 .net
あの証明は美しくない
5 １３２人目の素数さん[sage] 2011/01/23(日) 19:07:57 .net
美しくないけど、認めざるを得ない…ってかｗ
6 １３２人目の素数さん[sage] 2011/01/23(日) 20:13:30 .net
そのうち量子コンピューターが出て来て
簡単に解決できちゃうような希ガス
9 １３２人目の素数さん 2011/01/23(日) 23:13:56 .net
「作図」を定規とコンパスによるものに制限するのと同様に、
コンピュータを用いないものに制限したければ、それもありだろうね。
11 １３２人目の素数さん 2011/01/24(月) 13:30:02 .net
どうでもいけど、4色問題っての、地図屋さん以外に、なんか役立つ事あるの？
12 １３２人目の素数さん[sage] 2011/01/24(月) 15:12:49 .net
>>11
携帯電話の基地局配置
17 １３２人目の素数さん[sage] 2011/01/26(水) 00:06:52 .net
てっきりアルゴリズムがあるもんだと思ってた
24 １３２人目の素数さん 2011/01/27(木) 14:02:14 .net
だから、数学論文は、自然言語を廃して、全部、形式言語で書けと言ってるのに。
31 [―{}@{}@{}-] １３２人目の素数さん 2011/01/28(金) 01:28:10 .net
コンピュータプログラムやハードウェアなんてバグがないことを証明するのは
プロでも無理。事実バグがないプログラムなんてないと言われている。
そして、OSなどでは毎日のようにバグが報告されてそのたびに修正パッチが出てる。
32 １３２人目の素数さん[sage] 2011/01/28(金) 01:31:47 .net
人間の脳にバグがないことを証明するのは医師でも無理。
事実、毎日基地害が発生しており、健常者でも幻覚や幻聴を感じることがある。
さらに、錯覚は人間の脳のスペックとして避けられないエラーである。
要するに、いくつもの方法でチェックするしかないんじゃないの？
36 １３２人目の素数さん 2011/01/28(金) 08:32:16 .net
ぺれる万の論文が正しいことを検証するのに一年かかったよな
仮に100人の数学者が読んで議論して正しいとわかったとしても、誰か別の奴が間違いを示す可能性は否定できないでしょ、少なくともその100人の検証で完全に正誤が保証されるものではない。
本質的にはこれなんだよ。コンピュータ使った証明だとしてもな。
だから必要とされるのはコンピュータも人間の検証も不要なくらいエレガントで簡潔な証明。
つまりコンピュータで数え上げたり人がいちいち時間をかけて検証するような証明は、証明としては間違いないけど、まだまだ未熟な証明ってことだ。
39 １３２人目の素数さん[sage] 2011/01/30(日) 14:24:53 .net
全ての命題に、必ずしおエレガントな証明が存在するとは限らないだろ。
100億通りのパターンをしらみ潰しで調べて
ようやく証明できるような命題があったっていいじゃん。
むしろそういう命題にも目を向けてこそ
数学の世界の幅が広がるとは思わない？
10通りの場合分けですむ問題をエレガントと感じ、
100億通りの場合分けが必要な命題を未熟と感じるのは
結局は人間の脳みそのスペックの問題でしかないわけで、
そういう制約のないハイスペックな宇宙人がいたとしたら、
人類を差し置いて、どんどん新しい命題を発見してるかも知れないだろ？
40 １３２人目の素数さん[sage] 2011/01/30(日) 15:26:18 .net
それは確かだが四色定理にエレガントな解答が本当に無いのかどうかはまだ分かってない
41 １３２人目の素数さん[sage] 2011/01/30(日) 15:52:29 .net
別にエレガントな証明が存在するかどうかは問題でないんでない？
私としては紙と鉛筆を使うか、コンピューターを使うかの違いで、そこに壁はないと思うんですよ。
「上式を計算すると下式になり～」って証明があったとしても
第三者がそれをチェックするには、やっぱり紙と鉛筆を、あるいは計算機を用意しなきゃいけいないわけで、
原始人からしてみたら「紙と鉛筆を使わなきゃ追証できない証明なんて証明じゃない」とうつるんじゃないかな。
現代になってそれが
「上プログエラムを実行すると、下の結果になるので～」という証明に進化したのだと思えば
それほど違和感はない気がする。
46 １３２人目の素数さん[sage] 2011/02/09(水) 05:03:24 .net
他の分野・問題にどれだけ貢献したのかってのもエレガントさに含まれるよね？
49 １３２人目の素数さん[sage] 2011/02/14(月) 21:57:05 .net
>>46
全く関係ない。
52 １３２人目の素数さん 2011/05/05(木) 15:03:46.15 .net
例えば、フェルマーの大定理一つとってもそうだろ?
あれをコンピューターに突っ込んで、
でだらだらと長い意味不明の記号列が出てきて証明できました。
ワー凄い。
そんなことで満足していたら、今日ほど整数論が発達することもなかったとおもう。
様々な概念を導入して、問題を少しずつ理解していく作業が今日の整数論に大きな影響を与えた。
それを放棄してしまったら数学は大事なモノを失うことになる。
いや、もしそんなコンピュータ証明が可能なら、
整数論の発展自体無意味なのかもしれないが、
少なくとも、今日ほど数学は整数を「理解」することができなかったと思う。
そうなると数学の価値とはなんなのかという哲学的問題にぶち当たると思う。
そしてその答えこそが上で書いたこと。
それは数学に限った話じゃなく、あらゆる理学に言えること。
目的はあくまでも無知な人間が理解できるようになること。
>>44は一体数学の何が面白いと思っているの、何が目的だと思ってるの?
53 １３２人目の素数さん 2011/05/05(木) 15:05:15.68 .net
コンピュータの証明を認めるのは、
古典幾何学の問題を座標を入れて腕力で解くかのごとき暴挙だと俺は思うがね。
そんなことをしていては、問題や定理の本質には迫れないよ。
証明というものの価値は正しさの保証だけじゃない。他の定理との関係や必要な道具、
問題の本質を垣間見る為のものでもある。
定理を道具として使うにしても、その本質や背景を証明を通して理解していた方がいい。
少なくとも純粋数学的には認めてはならないと思う。
工学的応用に特化した分野だけでやって欲しい。
(もちろん、人間が呼んで理解できる範囲内の証明だったり、そのように加工した物ならその限りではないが)
そして、もし今の数学が、人間が理解できる範囲内での道具立てや定理がほとんど網羅され尽くして、
もうコンピュータに頼るしかないという状況なのだとしたら数学はオワコン。
55 ID:8/lKNVnj 2011/05/05(木) 16:22:18.57 .net
アルゴリズムが正しい事を証明できたなら、それを使った証明も正しい。
できないなら証明じゃない。
もし、証明できてないアルゴリズムによる「証明」があったとして、
それを多数の人間で検証したのなら、証明したのはコンピュータじゃなく検証した人間。
で、どこまで行ってるの？
58 １３２人目の素数さん[sage] 2011/05/23(月) 13:42:53.53 .net
たとえばカタラン予想のような自然数に関するある数式の予想があったとして
それの下限、上限がわかったらあとはしらみつぶしでの攻略もありえるわな
でもよりエレガントな方法を探すことで他の数学の分野へのつながりが
見出され数学的な発見があることもあるのでそれはそれで価値があるよね
73 １３２人目の素数さん[sage] 2011/09/25(日) 10:29:12.14 .net
昔みたいに一部の人しか扱えないコンピュータでないと
証明できないって状況は問題だと思ったな。
そりゃ「紙と鉛筆さえあれば誰でもできる」ていう数学の
良さに真っ向から対立してるからな。
でも今じゃその辺のパソコンで数十分で確認できること考えりゃ、
逆に人間による場合わけより精度高いだろって気にはなる。
74 １３２人目の素数さん 2011/09/25(日) 11:08:45.71 .net
「紙と鉛筆さえあれば誰でもできる」といいだしたのが
誰だかしらないが、それは数学の性質でもなんでもないな。
75 １３２人目の素数さん[sage] 2011/09/27(火) 12:18:43.43 .net
少なくとも数学の定義には「紙と鉛筆だけでできる」は含まれないだろう
76 １３２人目の素数さん 2011/10/10(月) 10:19:03.80 .net
組み合わせの問題でも全部書き出せば丸くれる。
78 １３２人目の素数さん[sage] 2011/10/11(火) 15:32:45.94 .net
>>76
それが全部である（書かれていないものはない）という証明がいるだろう。
なくても○をくれるのはおまけと言うか、サービスと言うか
答があってりゃ考え方はどうでもいいという時だけだろう。
79 １３２人目の素数さん 2011/10/16(日) 13:46:10.84 .net
そこまでひねくれてないよ。
物理なんか少数第一位まであってればしきなしでも○くれる。
80 １３２人目の素数さん[sage] 2011/10/16(日) 14:42:19.52 .net
それは 「答があってりゃ考え方はどうでもいいという時」なんだよ。
参考文献
