05/09/06 23:35:12
これが可能になったら数学者という仕事が無くなっちゃうの？
2:１３２人目の素数さん
05/09/06 23:36:59
2
3:１３２人目の素数さん
05/09/07 00:22:52
定理の自動証明が実用レベルに達してるなら他の大抵の仕事も実用レベルに達する。
その時にコンピュータには出来ないような新しい仕事を見つけられなければ
数学者だけでなく殆どの人間の仕事が無くなる。
4:１３２人目の素数さん
05/09/07 00:34:23
で、
コンピュータによる定理の自動証明ってどうやるのさ？
5:１３２人目の素数さん
05/09/07 10:58:40
趣旨とは違うが、「A=B」のような方向はもう少し発展すべきだと思う。
6:１３２人目の素数さん
05/09/07 12:43:47
ゲーデルの考えが正しいとすると、機械には数学者と同じレベルの証明は、
永久に出来ないだろう。
7:１３２人目の素数さん
05/09/07 12:53:17
>コンピュータには出来ないような新しい仕事
何が「美しい」か見極める事(新しくないけど)。
コンピュータの万能性の可能性を否定するにはそれだけで十分。
8:１３２人目の素数さん
05/09/07 13:35:03
主観がない、ということか。
9:１３２人目の素数さん
05/09/07 18:10:37
数学の概念を全て「記号」であらわすというのはライプニッツの目指したもの。
それを2進であらわせれば、コンピュータに数学をやらせる土台ができるかもな～。
10:１３２人目の素数さん
05/09/07 18:13:06
可能にはなると思うが、
「美しい証明」になるかどうかは別問題。
11:１３２人目の素数さん
05/09/07 18:13:47
既にある証明のデータベース化は進んでないの？自動証明による証明の再現という意味なのだけど。
12:１３２人目の素数さん
05/09/07 18:23:54
意味が概念として理解できなければ組合せの爆発により証明が終了しない。
13:１３２人目の素数さん
05/09/07 20:16:39
数学にも哲学にも通じてる情報科学のあったまぃー人が解決してくれるんでしょ
14:１３２人目の素数さん
05/09/08 00:23:02
以下マジレス
コンピュータによる定理の自動証明は今のところ「少し可能」という状態です。
事実、コンピュータで自動証明された定理も存在します。ただ、その証明はおせじにも美しい証明とはいえないが…
証明の内容は忘れたが、こんなことを前期の授業でやった。
15:１３２人目の素数さん
05/09/08 00:48:41
四色問題か
16:１３２人目の素数さん
05/09/08 01:31:06
>>15
たしか、二等辺三角形がどうたらってやつだった
四色問題は異論があるから微妙じゃない?
17:１３２人目の素数さん
05/09/08 03:48:11
４色問題は、地図を幾つかのパートに分割して、
その全てのパートに対して定理が成り立つことを確認する所を
コンピュータにやらせたんだったっけ？
この場合、コンピュータは人間の作ったアルゴリズム通りに動作しているだけなので、
「自動」証明とは言い難いなぁ。
てか、自動証明って何？コンピュータが1から全部証明やってくれることでしょ？
18:１３２人目の素数さん
05/09/08 07:33:41
四食問題は単に機械的にチェックできる部分をやらせただけなのでは。
微分方程式の数値解を計算機で出すか手計算でやるかの違いみたいな感じがする。
普通の自動証明というと、推論規則と命題を与えてその証明を作らせることかな？
19:１３２人目の素数さん
05/09/08 08:47:53
定理の自動証明は公理から出発して定理が導けるまで動作を続けるか、
定理から証明に必要な公理を導き出す。
20:１３２人目の素数さん
05/09/08 11:02:02
>>19
基本的には￢（公理⇒定理）から自動的に矛盾を導く。
証明が存在するなら、矛盾が導ける。
しかし、存在しない場合にはプロセスが終了しない可能性がある。
21:１３２人目の素数さん
05/09/08 16:06:50
>>20
それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
例えば宇宙の原子の数なんて10^50程度のオーダーしかない。
ちょっと難しい定理の機械証明の探索論理ステップ数なんて
そんなオーダーの組合わせ数じゃ済まないんじゃないの？
22:１３２人目の素数さん
05/09/08 16:45:14
「こういうときにはこの定理を用いる場合が多い」っつー傾向というのがありまして、
そういうメタ知識を用いると、かなりよくなります。
23:１３２人目の素数さん
05/09/08 18:01:02
>>22
それは人間が発見した定理を利用するということ？
それはちょっとズルイというか、やっぱ人間が必要なんじゃないかと
24:１３２人目の素数さん
05/09/08 18:03:40
>>23
なんじゃそりゃ、
もしや0から全てコンピュータに行わせようとしてるのか？
過去の資産を生かさずしてどうする。
25:１３２人目の素数さん
05/09/08 18:08:21
いつまでも人間が面倒みなけりゃならないなら、こっちこそなんじゃそりゃ
と言いたくなるな
26:１３２人目の素数さん
05/09/08 18:25:38
コンピュータは所詮道具なんだよ。
人間がやる定理証明に役立ってくれればいいの。
なんでもかんでもコンピュータにやらせる必要は無いの。
27:１３２人目の素数さん
05/09/08 18:25:42
とりあえず定理のデータベースを作ってくれ。
28:１３２人目の素数さん
05/09/08 18:31:02
>>5
A=B？
29:１３２人目の素数さん
05/09/08 18:35:36
>>26
それで役立つんかい？
人間が証明出来ない定理をコンピュータが証明してくれるとか？
30:１３２人目の素数さん
05/09/08 19:41:41
>>1
正しい定理を見つける仕事は残るだろう。
31:１３２人目の素数さん
05/09/08 20:02:07
ときたまジョブをチェックする仕事は必須
32:１３２人目の素数さん
05/09/08 20:08:24
人間に証明出来ない問題がコンピュータに証明出来るわけないわな。
コンピュータなんてただ計算が速いだけだし。難しい予想なんて解こうものなら既存の数学では無理な場合もあるし、
コンピュータがその道具を作っていくなんてまず不可能じゃね？
33:１３２人目の素数さん
05/09/08 23:08:57
人間だろうがコンピュータだろうが鼠を取るのが良い猫だ。
34:１３２人目の素数さん
05/09/08 23:14:10
コンピュータに快楽と苦痛を与えればなんでも出来る。
35:１３２人目の素数さん
05/09/08 23:57:12
オダインに頼め。
エルオーネの能力に比べれば、証明なんて
36:１３２人目の素数さん
05/09/09 01:31:54
>>34
強化学習も結局はx^nオーダーの計算量となるわけで
37:１３２人目の素数さん
05/09/09 01:36:53
追試・データベース化、翻訳などに役立つであろう。
38:１３２人目の素数さん
05/09/09 05:54:41
合流性とか停止性とかいう話があったよね＞証明系
39:１３２人目の素数さん
05/09/09 13:21:38
おまえらPrologは知ってるよな？
40:１３２人目の素数さん
05/09/09 13:32:45
ああ、あの失敗したプロジェクトで使われた言語ね
第五世代コンピュータ開発計画とかいう税金のムダ使いで
41:１３２人目の素数さん
05/09/09 13:55:07
プログラミング言語で一種のファッションだろ？
42:１３２人目の素数さん
05/09/09 14:14:59
プログラミング言語は流行廃りが激しいから、数学者が勉強すべきものではないだろう。
43:１３２人目の素数さん
05/09/09 14:37:44
自動証明⊆人工知能
と言える？
人間並みの人工知能ができれば、自動証明もできるはず。
44:GiantLeaves ◆6fN.Sojv5w
05/09/09 17:03:36
証明作成のアルゴリズムとして、どんな方法がありうるのか？
検索の枝きりが難しいと思う。
45:１３２人目の素数さん
05/09/09 17:40:48
あ、今アリゴリズム体操おわっちゃった。
46:１３２人目の素数さん
05/09/09 19:04:07
こっち向いて二人で前ならえ
あっち向いて二人で前ならえ
47:１３２人目の素数さん
05/09/09 22:58:51
>>28
> >>5
> A=B？
ググれ。
48:１３２人目の素数さん
05/09/09 23:15:49
>>47
URLﾘﾝｸ(www.google.com)
URLﾘﾝｸ(www.google.com)
URLﾘﾝｸ(www.google.com)
ﾊｧ?
49:１３２人目の素数さん
05/09/09 23:30:32
ほらAIってあれだろっ！ドラクエ４に搭載の…
50:１３２人目の素数さん
05/09/10 06:22:49
ボスに向かってザラキを唱えるやつか。
51:１３２人目の素数さん
05/09/10 10:43:48
>>48
キミはgoogle の使い方を知らない。
52:１３２人目の素数さん
05/09/10 11:07:15
この分野は日本では信州大が一番進んでいる
ようだよ。
お前らが大好きな数研の教科書書いてる方が
精力的に進めている
53:１３２人目の素数さん
05/09/10 11:46:30
>>52
mizarは"theorem prover"ではなく"proof checker"ですよ。
checkerでさえ現状ではライブラリ不足で実際に数学では使えないでしょう。
54:48
05/09/10 13:48:10
>>51
ではどのようにすればA=BでGoogleで検索できるか教えていただけますか？
(´-`).｡ｏO(二重引用符でくくれとかそういうｵﾁかな？)
55:名無しさん＠そうだ選挙に行こう
05/09/10 23:49:29
挑発したら教えてもらえなくなるよ
56:48
05/09/10 23:53:25
はいはいヽ(´ー`)ﾉ
57:名無しさん＠そうだ選挙に行こう
05/09/11 19:18:21
>>53
ライブラリ不足かどうかは知らんが、そもそも現実の数学研究で使えるような
表現力を持つ言語を処理させるのはきついんじゃなかろうかと思う。
>>54
俺も気になる。
「A=B」みたいなのをキーワードにしてGoogleで有意義な情報を引き出せるのか？
まあ元々の発言(>>5)の言わんとするところはわからなくもないが。
58:名無しさん＠そうだ選挙に行こう
05/09/11 22:54:00
コンピュータにPeano算術での自動証明プロセスを与えて、
しらみつぶしで￢(0=0)の証明を探索させたら、
もしかしたら有限時間内に「証明あり」って出力が返る可能性がある?
もしそうなったらどうなるの?
59:名無しさん＠そうだ選挙に行こう
05/09/11 23:03:14
>>58
PA が矛盾してるならあるかもね
60:名無しさん＠そうだ選挙に行こう
05/09/11 23:31:38
>>59
こえー。そしたら帰納法使った証明が全ておじゃんだしZFとかも壊滅だし。
>>58の自動証明を延々走らせてる不信心な暇人っていないのかな。
61:１３２人目の素数さん
05/09/12 08:30:11
A=B 等式証明とコンピュータ, 1997 トッパン
トッパンが2000年に出版事業から撤退したため、あまり知られてない。
幸い原本がpdfで公開されている。クヌースによる序言だけでも読むことを勧める。
URLﾘﾝｸ(www.cis.upenn.edu)
62:１３２人目の素数さん
05/09/12 17:01:24
>>21
＞それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
人間もバカチョンでしらみつぶしに探してる。意識してないだけ。
人間が証明を見つけるまでの間にもそれこそ長い年月を必要としている。
今のコンピュータよりも人間のほうが優れているかもしれんが
それこそ非常に長い時間をかけた進化の結果である。
63:１３２人目の素数さん
05/09/12 17:05:14
>人間もバカチョンでしらみつぶしに探してる。意識してないだけ。
嘘だろ
64:１３２人目の素数さん
05/09/12 17:12:09
>>63
残念だが本当だ。
ところで、誰かTarskiの量化記号消去について簡単に説明してくれ。
65:１３２人目の素数さん
05/09/12 17:21:28
>>64
話をそらすなよ。しらみつぶしなわけないだろ
しらみつぶしだったら時間がかかりすぎ。
66:１３２人目の素数さん
05/09/12 17:34:00
>>65
いや、そのくらい時間がかかるのが当然なんだ。
それより、質問したことについて知らないなら黙っててくれ。
無知な奴と遊んでる暇はないんだ。
67:１３２人目の素数さん
05/09/12 17:41:41
>>66
時間がかかりすぎというのは１００年とか２００年のオーダー
じゃないんだよ。現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。
68:１３２人目の素数さん
05/09/12 17:43:51
>>67
＞現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。
君以前の人がそうしている。
君がその知識を利用しているときに
そのことを意識できないだけ。
69:１３２人目の素数さん
05/09/12 17:58:40
>>68
過去の知識といっても膨大。
その膨大な知識をしらみつぶしに調べてるわけじゃない。
70:１３２人目の素数さん
05/09/12 18:02:23
彼の「しらみつぶし」って単語の定義が俺様独自定義なんだろ
71:１３２人目の素数さん
05/09/12 18:26:37
昔の人がすでにしらみつぶしに調べてきたから今の人はそうする必要がないという理屈だな
72:１３２人目の素数さん
05/09/12 18:51:19
例えば将棋で次の一手をしらみつぶしで探せるはずがない。
それと同じで証明もこうすればよさそうだ、とある程度見切りをつけて行っているはず。
直観力+構成力+知識・経験が物を言う。
73:１３２人目の素数さん
05/09/12 18:54:43
>>71
その昔のひとが得た結果の組み合わせの数だって膨大。
それを、しらみつぶしに調べてるわけない。
74:71
05/09/12 19:28:09
>>72
我々がそういう力を持ってるのは昔の人がしらみつぶしにやって得た知識を
受け継いでるからだと考えることもまったく不可能なわけではないんじゃない？
>>73
まあそうかもしれないとは思うけど、自信を持って言い切れる理由があるの？
一応言っとくと、>>62 を積極的に支持するわけじゃないよ。
けど、間違いだという根拠も持ってないし、
部分的には正しいように思えるからあえてこういうレスをしてみた。
75:１３２人目の素数さん
05/09/12 20:19:54
コンピュータで証明するときに、あらかじめ「知識」のデータベースを入れて
それ使って証明しても「しらみつぶしで証明しました」って言うわけか？
76:１３２人目の素数さん
05/09/12 20:31:51
しらみつぶしって言うのは、たとえて言うなら、10回戦のトーナメント方式の1回戦から全ての対戦を行うことに例えれば。
知識があるっていうのは、経験則でこの対戦は無いってシードの部分がいくつかあって考慮する必要のない部分があるってことでしょ。
77:１３２人目の素数さん
05/09/12 20:39:10
今使ってるパソコンでも、π=3.14・・・とかはいちいち計算しないで使われてるんだろ？
78:１３２人目の素数さん
05/09/12 20:39:15
意味を理解しているならばしらみつぶしに探索しなくてよい。
79:１３２人目の素数さん
05/09/12 21:35:02
おまえら、せめてヒューリスティックスって言葉使えよ・・・
80:１３２人目の素数さん
05/09/12 21:37:47
うむ、そういえばそんな言葉があったな。
最近使ってなかったせいか忘れていた。
81:１３２人目の素数さん
05/09/12 21:39:37
>>77
ヒューリスティックスなしらみつぶしで、「知識」のデータベースを
元に計算してまつ
82:１３２人目の素数さん
05/09/12 21:43:39
>>81
ﾜﾛｽw
83:１３２人目の素数さん
05/09/13 13:45:06
とにかくこのスレは不毛。人間の知能の仕組みなんて誰もなーんも
わかっちゃいない。それをコンピュータでシミュレート出来るわけがない。
映画とかＳＦでは人間なみのロボットが出てくるけど、そんなのまさに
夢物語。人口知能の研究者ってのは鉄腕アトムの読みすぎ。
定理の証明というのは人間の知的能力の一部だけど、まるで解明
84:１３２人目の素数さん
05/09/13 13:49:55
書き込んでる最中に暗殺された>>83のご冥福をお祈り致します。
85:１３２人目の素数さん
05/09/13 16:01:37
>>72
＞証明もこうすればよさそうだ、ある程度見切りをつけて行っているはず
それはしらみつぶしとは矛盾しない。
単に深さ優先探索ではないというだけ。
86:１３２人目の素数さん
05/09/13 16:04:24
>>83-84
ﾜﾛｽw
87:１３２人目の素数さん
05/09/13 16:04:25
＞人間の知能の仕組みなんて誰もなーんもわかっちゃいない。
＞それをコンピュータでシミュレート出来るわけがない。
･･･というより、シミュレートしていたとしても
それに気づくことができないというべきか。
ところで数学の定理の証明がすばらしいものだ
という考えは数学をやっている人間の個人的感情
に過ぎない。
88:１３２人目の素数さん
05/09/13 16:30:30
>>87
定理の証明が出来るということは不思議な能力だという考えは？
89:１３２人目の素数さん
05/09/13 16:38:48
>>88
不思議とは無理解のことである。
90:１３２人目の素数さん
05/09/13 17:06:41
この場合は無理解というより不可解
91:１３２人目の素数さん
05/09/13 17:51:05
地球の原子すべてをシミュレーション出来るコンピュータが出来たら生物はもちろん文明さえもシミュレーション
出来るのではないか。
92:１３２人目の素数さん
05/09/13 18:10:57
>>91
データをどうやって入れるんだよ
93:１３２人目の素数さん
05/09/13 18:15:55
>>91
そのコンピュータは自分自身をシミュレートするのか？
94:１３２人目の素数さん
05/09/13 18:53:47
哲学的な問いでなかなか面白いでつね。
95:１３２人目の素数さん
05/09/14 00:02:45
>>94
チューリングマシン
とか
停止問題
でぐぐってみ。否定的な結論が出るから。
96:１３２人目の素数さん
05/09/14 06:20:52
証明すべき命題をどう符号化するか、という問題がまずある。
もし、すべての数学定理が計算機で証明できるならば、
たったひとつのアルゴリズムから、次々に定理を自動生成できるんじゃなかろうか？
そんなアルゴリズムが果たして存在するのか？
97:１３２人目の素数さん
05/09/14 07:14:49
>>96
ZFC を計算機で書けばいいわけだから原理的には余裕でできる
けどなんか工夫しないと時間かかりすぎて意味のある定理はほとんど出ないと思う
98:１３２人目の素数さん
05/09/14 07:39:17
>>96
くそ定理は山程合成出来る。
99:１３２人目の素数さん
05/09/14 09:30:09
人間機械論を否定したゲーデルの論文があると聞いた。
彼の不完全性定理を基にしている。
人工知能を研究している人なら知ってるよね？
100:１３２人目の素数さん
05/09/14 10:21:30
>>93
コンピュータをシミュレーションするコンピュータはターゲットのコンピュータより
メモリは大きくスピードも速くなければならない。
101:１３２人目の素数さん
05/09/14 10:31:37
そんなことより地球シミュレータのデータのほうが問題だろ。
全ての原子のデータなんてわかるわけがない。
可能性があるとしたらBig Bangのシミュレータ。
仮に出来たとしても地球が出来るまで相当時間がかかるｗ
102:１３２人目の素数さん
05/09/14 18:28:09
>>100
確かにメモリは大きい必要があるが、
スピードに関しては遅くても構わない。
ただし、もちろん実物より遅くなってしまう。
用途によっては実物より遅くても、結果の再現が得られれば良い場合もある。
例えば新しいCPUの回路設計など。
103:１３２人目の素数さん
05/09/14 18:29:11
>>98
文字通りトリビアの泉になるわけだな……。
104:１３２人目の素数さん
05/09/14 18:46:14
山田君、座布団1枚もっていki（略
105:１３２人目の素数さん
05/09/14 19:38:13
停止性問題しかり、ﾃﾞｨｵﾌｧﾝﾄｽ方程式しかり、計算機で証明できない問題はたくさんあるわけで。
「定理」は有限文字列で表現できるから
「この世のすべての定理」を列挙することは一応できるけど
それらすべての真偽を判定することはできないと言うことか。
106:１３２人目の素数さん
05/09/14 22:21:08
>>105
証明できないものを定理とは呼ばないんじゃ？
それでも定理全てを列挙することは出来るが。
107:１３２人目の素数さん
05/09/14 22:29:02
最近のコンピュータ将棋って結構強いよね。
ルールや対局データを与え、アマチュアには勝てるようにプログラムされている。
自動証明も同じようにできそうだけど、案外自動証明を研究されている方がプログラミングが不得意なのかもしれないよ。
私の従兄弟は数学のセンスは凄いのだけど、プログラムはてんで組めないんだよね。
108:１３２人目の素数さん
05/09/14 22:34:56
>>106
ゴメンナサイ。「定理」ではなく「命題」と言うべきでした。
109:１３２人目の素数さん
05/09/14 22:41:57
一応確認すると、定理全体の集合は recursively enumerable ですよね？
110:１３２人目の素数さん
05/09/14 22:49:06
>>107
自動証明は将棋みたいに特化したものじゃないから同じようには無理だと思うよ。
あと数学のセンスとプログラム組む能力は関係ないと思う。
そもそもプログラムと一括りにしているが、使う言語がCかLispかでも
だいぶ違うんじゃないか？
ちなみに俺の友達には、高校数学のアルゴリズムの項目は
BASICじゃなくて関数型言語を使うべきとかいってるヤツがいるぞ。
>>108
どんまい
111:１３２人目の素数さん
05/09/14 22:50:40
>>109
そうだよ
112:109
05/09/14 22:53:18
そうですよね。
>>105を見るとそうでないように読めたので気になったので。
113:109
05/09/14 22:57:33
あれ、そうでないように読めたのが勘違いか。
有限時間内に真偽を判定することはできませんね。
どうもすいません
114:１３２人目の素数さん
05/09/14 22:58:33
>>110
高校数学の本閲覧したけど…１社だけ、JavaScriptだなｗ
確かに、関数型を通り越して、オブジェクト指向言語だわ。
で、こんなの勉強していちいち
<html><head>
<script language="JavaScript">
<!--
スクリプト本体
//-->
</script>
<head>
なんて、訳もわからず入力しているの想像すると…コピペするにして
も、何か非常に可哀想になってくるんですけど。
そりゃ、「極一部」のソフトで飯食おうとするヤツは別だろうけどさあ。大体、
そんなヤツは学校じゃなく自力で覚える！
115:１３２人目の素数さん
05/09/14 22:59:36
情報科学の人も、プログラミングできる人の方が少数派なんでしょ？
116:１３２人目の素数さん
05/09/14 23:03:04
>>112
r.e.だけだと偽かどうかを判定する手続きが止まらない可能性があるから
そういう意味では真偽を判定出来ないとも言える。
decidable(=recursive)ではないってことだ。
117:１３２人目の素数さん
05/09/14 23:08:18
>>114
＞高校数学の本閲覧したけど…１社だけ、JavaScriptだなｗ
マジ？！！
これで勉強させられるヤツら悲惨だな…。
本質的でない部分が多く含まれる上に、どうせ教える側も良くわかってないんだろうし。
118:１３２人目の素数さん
05/09/14 23:20:28
>>117
まともな、高校数学教師なら、その教科書のその部分は「飛ばすべき」だ。
後で、校長や教頭から文句がくるやも知れないが、その方が「良心的」だと思う。
119:１３２人目の素数さん
05/09/15 08:52:32
>>110
Ｃ言語でLispコンパイラを書けばいいじゃないか。
120:１３２人目の素数さん
05/09/15 08:55:41
>>119
コンパイラを書くと何がいいの？
121:１３２人目の素数さん
05/09/15 09:08:46
>>105
>「この世のすべての定理」を列挙することは一応できるけど
「この世のすべての定理」って、意味がよくわからない。
現在人類に知られている定理のすべてっていう意味？
因みに、当然だけど、可算無限集合の要素を有限時間内にすべて列挙する
ことは出来ない。
122:１３２人目の素数さん
05/09/15 09:34:54
>>99
>人間機械論を否定したゲーデルの論文があると聞いた。
岩波の文庫本だったか啓蒙的な本を読んだだけなので詳しいことは
わからないけど、ゲーデルの趣旨は多分、以下のようなことだろうと
想像する(この想像が間違っていることも大いに有り得る)。
不完全性定理は機械には証明できない。よってそれを証明した
人間(ゲーデル)は機械では有り得ない。
123:１３２人目の素数さん
05/09/15 10:52:13
人間機械論は人間と機械論が正しいと聞いたが、
124:１３２人目の素数さん
05/09/15 10:58:28
それはどうでもよくて、>>122のゲーデルの趣旨は、人間の頭脳は
チューリングマシンのような機械ではないということ。
125:122
05/09/15 11:50:58
>>122
>不完全性定理は機械には証明できない
自分で言い出してなんだけど、これ本当かな。
原理的には機械にも可能なような気もするな。
もしそうならゴメン
126:１３２人目の素数さん
05/09/15 11:51:30
確かに人間の脳はチューリングマシンと違うよね。もしかしたらチューリングマシンにノイズの項を追加すると人間の脳と等価になったりして。ゲーデルはきっとノイズが大嫌いだよね（独断と偏見）。
ちょっと唐突だけど、ピタゴラス数（ ａ^2 + ｂ^2 = ｃ^2 ) の基本解についてはかなり昔から知られていたよね。
基本解を導く手順のなかに「ｃは奇数である」とか「ａかｂのどちらか一方だけが偶数」なんていうのが現れる。そして最後にいくつでも簡単にピタゴラス数を計算できる方法を導いている。「昔なのにすごいなぁ」などと感心したもんですよハイ。
ピタゴラス数の基本解の導き方は今の中学生でも簡単にできる問題なので、自動証明のプログラムの例題としても比較的簡単そうだし、もしかしたら既に誰かがやっていると思うんだけどなあ。でもニュースなどでこれに近いことすら聞いたことがないのですよハイ。
127:１３２人目の素数さん
05/09/15 12:32:01
あまり意識してないけど、俺が証明を考えるときは、たぶん、
その定理に使えそうな命題をいくつか組み合わせて推論し、
それが成功しないときは別の組み合わせを試す。つまり試行錯誤。
組み合わせというより、いろいろな方法と言ったほうがいいかもしれない。
定理によっては証明のパターンというものがある。
この種の定理にはこの方法を使うというような。
だから、問題を解く経験を含めた広い意味の知識というのは大きな要素
であるのは間違いないと思う。
128:１３２人目の素数さん
05/09/15 13:23:13
ある種のノイズが関係していることは十分考えられる。
量子力学的ゆらぎとか。
そのノイズによりひらめきが誘発されるとか。
129:１３２人目の素数さん
05/09/16 16:56:49
>>不完全性定理は機械には証明できない
>自分で言い出してなんだけど、これ本当かな。
もちろん初歩的な誤り。
不完全性定理は形式的証明が可能。
証明できないのはゲーデル命題。
もっとも、人間にも証明できないわけだが。
130:１３２人目の素数さん
05/09/16 22:46:54
例えば、三角形の定義を入力すると三角形に関するありとあらゆる定理（クソなのも含めて）を生み出す
ってことは出来るのかな？
131:１３２人目の素数さん
05/09/16 23:33:14
公理や推論規則も入力すればできる
132:１３２人目の素数さん
05/09/18 04:33:41
初等幾何の証明はどうするんだろう。
図は別に使わないだろうけど、補助線の考え方自体は要るよね。
あれは激しくセンスが必要な気がするんだが…。
133:１３２人目の素数さん
05/09/18 05:48:57
・・・え？
134:１３２人目の素数さん
05/09/18 11:17:39
ところで、数学の定理って有限？
135:１３２人目の素数さん
05/09/18 11:57:54
夢幻
136:１３２人目の素数さん
05/09/19 00:33:41
>>132
適当に総当たりで補助線引いてみて、過去の定理を当てはめることができるか、
総掛かりで検索する…とか。
137:１３２人目の素数さん
05/09/19 11:58:12
>>134
家産
138:１３２人目の素数さん
05/09/19 15:04:55
>>132
証明の方法まで指定するのか？
コンピューターで計算するんなら、座標やベクトルを使うことになるんじゃないのかな。
139:１３２人目の素数さん
05/09/21 14:20:02
＊ 任意の命題を証明するアルゴリズムは無い。
この前提となっているのは、「アルゴリズム」として、
有限長のものをどんな命題にも先立って与えるとしたら、
ということです。
命題を与えられてからそれを観た後であれこれとアルゴリズムを
生成していって、一般には有限個とは限らずに無限のアルゴリズム
列を作っていきながら判定を試みるというやり方であれば、
どうなるのかについては証明法の範囲外であると思います。
（この場合、「アルゴリズム」の列全体は可算ではないのです）
140:１３２人目の素数さん
05/09/21 15:46:10
問題：
数学的帰納法で証明できる自然数の定理は、
すべてコンピュータで自動証明できるか？
141:１３２人目の素数さん
05/09/21 22:05:49
Ｎｏ かな？
ペアノの公理系の帰納法は、自然数の集合あるいは自然数の命題に関する公理。
ペアノ算術の帰納法は、初等的命題に関する公理スキーマであり適用範囲が制限される。
このため人間が数学的帰納法により証明できる自然数の定理であっても、
その証明を一階述語論理＋ペアノ算術で形式化できない可能性がある。
142:１３２人目の素数さん
05/09/22 08:03:10
Ｙｅｓだな！
ペアノの公理系は形式化されたもの。
証明があるなら当然コンピュータで自動証明できる。
しかし証明がない場合には延々と止まらない。
したがって、有限時間で全ての定理を
証明し切ることはできない。
143:１３２人目の素数さん
05/09/22 15:14:37
人間だって有限時間で全ての定理を証明する事はできないジャン
144:１３２人目の素数さん
05/09/22 18:10:03
>>143
人間ならできる！といった覚えは一度も無いが
145:１３２人目の素数さん
05/09/22 21:22:11
帰納法使えばいいじゃない
146:１３２人目の素数さん
05/09/23 05:21:34
>>139
それは命題を入力として証明手続きを列挙する手続きの存在を仮定してるから
結局同じことなんだが。
あと真でない命題を入力した時に有限時間内に終わらない可能性がある。
最終行の可算は有限の間違い？
147:１３２人目の素数さん
05/09/23 15:41:29
いや、ちょっと架空の話で例示してみよう。
（本当はこういうことはないのだが、N文字で書かれた任意の命題を
証明することのできる・あるいは否定できる手続きのプログラムで
１０＾１０＾N文字以内で書けるものが常に存在する、
というようなことがあったと仮にしてみよう。もちろん嘘だが）
もしもそうであれば、
そのとき、ある任意の命題（その長さをN文字としよう）
が与えられたとして、それから始めて、１０＾１０＾N文字以内の
プログラムをすべて列挙して調べれば原理的には答えがわかる
ということになる。
ところが、全く任意の命題が与えられるとするならこの方法は使えない。
なぜならNが事前には抑えられていないので、予め有限長のプログラムを
用意しておくなどということが出来ないのだ。
つまり、もしも、このような状況であれば、
やってきた入力を観た後からだと可能である。ところが
どんな入力が来ても処理できるように事前に準備することは
出来ない、のである。
148:１３２人目の素数さん
05/09/29 16:19:50
295 ：１３２人目の素数さん ：2005/09/29(木) 11:58:46
夫馬です。
黒木先生。この基礎論・計算科学屋を叩いて下さい。
「完全証明」という専門用語を使い、「今まで数学
的に完全な証明がなかった！」というように素人に
思い込ませる。コケオドシをやっています。ポモ的
です。やっつけて下さいな。
＞フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの
＞数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
＞工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との
＞約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
＞などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が
＞完成。中村教授らは「完全証明したのは世界初」としている。
URLﾘﾝｸ(www.mainichi-msn.co.jp)
149:１３２人目の素数さん
05/09/29 16:23:20
土建屋、宇沢、長谷川、黒木の数理物理、可積分系、表現論自体が
コケオドシだから、黒木にこいつらを叩く資格はないよｗ
150:１３２人目の素数さん
05/09/29 16:25:11
301 ：１３２人目の素数さん ：2005/09/29(木) 15:12:47
>>295
この中村って香具師、あほ鴨の仲間じゃねーか？
302 ：１３２人目の素数さん ：2005/09/29(木) 15:16:20
>>301
ポモ的なのに叩かないのは、そういう理由だったんだね！
土建屋＝宇沢＝長谷川＝黒木 ← 隠れポモ野郎
禿藁＝Ｕ健爾 ← 隠れポモ野郎
あほ鴨＝中村 ← 隠れポモ野郎
303 ：１３２人目の素数さん ：2005/09/29(木) 15:26:53
>>302 >>295
こいつらって、結局
ポモと同じでしょ。
＞そして、別の場所で、極端なことを言っているのではないかと非難された場合には、
＞3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。
URLﾘﾝｸ(www.math.tohoku.ac.jp)
151:１３２人目の素数さん
05/11/10 18:44:30
552
152:１３２人目の素数さん
05/11/10 20:55:41
記号論理学が嫌われるのは、命題という、数のようにモノと思いやすくない
ものまでＡとかＢとかいう記号で扱うことに対して、無意識の不安、抵抗
があるからであろう。
これを払拭させるには、まず。「命題はモノではない」ということを
明確に意識させたうえで、「それでも命題は或る意味でモノ扱い出来る」
ということを相当徹底的に理解させることが有効であろう。
尤も、この第２段階で徹底的に抵抗するような人物には、この教育法も
無力であろうが、記号論理学嫌いのほとんどは、第１段階によって、自分
の記号論理学嫌いの原因を明確に意識出来れば、次の第２段階も突破する
であろう。
そうなれば、定理の自動証明の基本構想の概念に到達し易くなるであろう。
このスレッドの話はそのあで始めるのが良いだろう。
153:１３２人目の素数さん
05/11/10 20:58:37
そのあで ー＞ そのあとで
154:１３２人目の素数さん
05/11/10 21:18:05
>>152
そういった内容は認知心理学でいうメタ知識に相当するから、
いわば「公理の公理」としておさえておくことが好ましい。
155:１３２人目の素数さん
05/11/10 22:11:50
記号論理学の見た目の記号がつまらん。
156:１３２人目の素数さん
05/11/11 17:49:54
記号論理学って嫌われてるのか？
どういう人に？
157:１３２人目の素数さん
05/11/12 07:28:14
大統一数学理論ってないですかね。
158:１３２人目の素数さん
05/11/12 17:40:12
人間の脳みそで出来るんだからコンピューターにだって出来るだろ
159:１３２人目の素数さん
05/11/12 17:44:11
今のコンピュータじゃかなり難しいだろ
160:１３２人目の素数さん
05/11/13 15:22:48
出来たとき有益で人々から感謝されるならば作る価値がある。
161:１３２人目の素数さん
05/11/16 20:43:05
不完全性定理の証明とか見るとわかるが
コンピュータに足りないのは定義を増やすという操作なわけだよ
162:１３２人目の素数さん
05/11/18 07:41:45
age
163:１３２人目の素数さん
05/11/18 07:44:37
定義を増やすぐらい出来ているが・・・
164:１３２人目の素数さん
05/11/18 07:50:48
融通が効くかどうかが重要なのね
165:１３２人目の素数さん
05/12/12 18:46:27
924
166:１３２人目の素数さん
05/12/12 19:03:53
コンピュータが出来てから１０年くらいたったころだから今から
５０年位前に計算機科学の有名な学者が１０年以内に定理の
自動証明が出来るだろうと予言した。だから専門家といってもなーんも
分かってないんだよ。現在だって同じ。
167:１３２人目の素数さん
05/12/12 22:52:38
しらみつぶしに証明のゲーデル数が小さい方から
定理を全て証明していくつもり、、だったんだろうかな
何の見積もりを間違えたんだろう？
実際の定理の複雑さか計算機のスピードか
168:１３２人目の素数さん
05/12/13 09:31:57
ノイマン式コンピュータじゃ無理だろ。
ま俺は専門家じゃないからあてにならないがｗ
今のコンピュータというのは原理的には５０年前と同じ、
つまりノイマン式。これをいくらいじっても無理だろう。
169:１３２人目の素数さん
05/12/13 14:34:14
四色問題はチェック作業を機械化しただけであり、自動証明とは言えない。
しかし証明に携わった人間によれば、時折コンピュータが
人間以上の「知性」を垣間見せることがあるという…。
170:１３２人目の素数さん
05/12/13 14:37:46
>>169
時折垣間見せるじゃ駄目だろ。俺みたいにチューリングテストに
パスしないと。
171:１３２人目の素数さん
05/12/13 17:18:15
Kingって結構チューリングテストに合格しなかったりしてｗ
172:１３２人目の素数さん
05/12/13 17:18:46
ってか自動証明の話してるときにチューリングテストの話せんでもいいだろ
173:GiantLeaves ◆6fN.Sojv5w
05/12/13 22:18:30
talk:>>171 何やってんだよ？
174:１３２人目の素数さん
05/12/13 22:22:56
いやいかにも
talk:>>とか自動生成っぽいなとか思ってｗ
175:１３２人目の素数さん
05/12/14 09:08:39
>>172
冗談通じないのね。
176:１３２人目の素数さん
05/12/20 06:34:18
定理の自動証明なんて散々研究されてる分野なんだが
なんで出来ないとか主張してる奴がいるんだ？
せめて「定理 自動証明」でググれ
177:１３２人目の素数さん
05/12/21 14:46:23
age
178:１３２人目の素数さん
05/12/21 15:21:45
>なんで出来ないとか主張してる奴がいるんだ？
(証明が自明な定理は除いて)出来てないから。
179:１３２人目の素数さん
05/12/21 17:38:44
研究されてるのと、実際に実現してるのは別だよね
AIも然り
180:１３２人目の素数さん
05/12/21 22:49:10
コンピュータのスピードさえ上がればえらいことになるだろ？
暗号だけじゃなくて定理証明も。
量子コンピュータとかが実用化したら、、、？
181:１３２人目の素数さん
05/12/22 01:48:46
そうかなあ、、結構オーダーが違うと思うけど、、
第一コンピューターがそんなに早かったら
気象学も分子生物学も量子化学も今より進歩してるはずだよw
182:１３２人目の素数さん
05/12/22 10:42:15
１８１の２行目以降は無意味。
183:１３２人目の素数さん
05/12/22 11:28:53
>>1
コンピューターが何かわかっていない。考える機械だとでも
思っているのか。人間が作ったソフトウェアを実行するのみ。
計算とかは得意だから全部計算してみるとか、数え上げるなんて
ことはできるだろう。いずれにせよ有限個のみ。
184:１３２人目の素数さん
05/12/22 21:44:13
人間の脳だって化学反応の連鎖で動いているだけだけどな
185:１３２人目の素数さん
05/12/22 23:19:51
人間が証明出来る数学の命題式も有限個にすぎない。
今までに書かれた全ての数学の論文、書籍を論理過程の
省略を無くして書き直したとしても、使われる文字の
総数は有限個に過ぎない。「任意の実数に対して成り立つ」
とかいう有限個の文字の思考で無限個のことが分ったつもり
になっているに過ぎない。
コンピュータによる定理の自動証明は可能と言ってよい。
ただコンンピュータの速度が飛躍的に増大すればいい。
証明された定理のうち、人間にとって意義あると思われる
ものを選び出すのは人間の仕事となるだろう。
コンピュータが脳と「同様に」働かなくても良い。脳が証明する
のと「同じ」定理を噴出しつづければばいい。
「ピッチングマシンが人間の投手と「同様に」働かなくてもいい。
人間が投げるのと「同じ」タマを発射すればいい。」
というのと同様。
186:１３２人目の素数さん
05/12/23 06:41:52
＞証明された定理のうち、人間にとって意義あると思われる
＞ものを選び出すのは人間の仕事となるだろう。
そんな100億（くらい少なけりゃまだ良いがｗ）の芥の中から
1個の宝石を選び出す仕事が成立すると思うのかねｗ
数学者の人生の99%は無意味な定理の吟味に費やされるぞｗ
187:１３２人目の素数さん
05/12/23 08:05:42
>人間が証明出来る数学の命題式も有限個にすぎない。
これはいいとしても
>「任意の実数に対して成り立つ」
>とかいう有限個の文字の思考で無限個のことが分ったつもり
>になっているに過ぎない。
実際どんな実数ほうりこんでも「任意の実数に対して成り立つ」
定理はなりたつでそ。しかも証明までされてるんじゃ文句言えない
でしょ。あなたは数学の証明で使われる論法はでたらめだと言いたい
のですか。コンピューターで片っ端から数を代入しても成り立つ
はずです。でもコンピューターでは有限の数しか扱えないので
無理数は扱えない。この辺がコンピューターの限界。
188:１３２人目の素数さん
05/12/23 08:13:55
>人間の脳だって化学反応の連鎖で動いているだけだけどな
これも科学者の作り出した単純な世界観にすぎない。
こんなもので普遍的に正しいものが捕らえられるだろうか。
進化論を全員まじめに信じるのは日本人だけで、科学先進国
欧米ではそんなこと全然ないということは知っておくべき。
189:１３２人目の素数さん
05/12/23 08:47:05
>>187
でたらめじゃなくて、有限個の文字で表現できる思考で
無限のことを考えて、その程度の思考でとらえられる
無限のからむ真理ぐらいまでしか分っていないと言って
るの。
人間が無理数を考える思考も、ある様式に則って表現
すれば、有限個の文字で表されるだろ。それをコンピュ
ータで扱うことも出来ることになるという筋。
これぞ記号論理の原理のひとつでしょ。これを拒絶する数
学屋が多い（？）のは不思議。
190:１３２人目の素数さん
05/12/23 08:47:28
＞でもコンピューターでは有限の数しか扱えないので無理数は扱えない。
代数的数なら頑張れば扱える気がするけどね
扱い方工夫すれば
>>188
＞進化論を全員まじめに信じるのは日本人だけで、科学先進国
＞欧米ではそんなこと全然ないということは知っておくべき。
欧米で進化論を真っ向から否定するのは、
プロテスタントの狂信者くらいしか居ない訳ですが、、
進化論は間違っている、なぜなら聖書に書いてないから、とか物凄く
「科学的」なことを言う人たちね
とりあえずおまいさんは「利己的な遺伝子」嫁
話はそれからだ
191:１３２人目の素数さん
05/12/23 08:55:10
コンピューターで扱っているのは有限の２進数だから
近似値としての無理数以外扱えない。無理数の近似値
は有限の数、すなわち有理数のなかで有限のものだけ
しか正確には扱えない。これで様子を調べるとか近似値
を求めることはできる。科学実験ではそれで十分かも
しれないが数学はそういう立場ではないでそ。
192:１３２人目の素数さん
05/12/23 09:02:15
>欧米で進化論を真っ向から否定するのは、
>プロテスタントの狂信者くらいしか居ない訳ですが
こういう風にカルトしか単純な科学的世界観を否定しない
などと思っているのは日本以外の文化を知らないから。
ニュートン力学の神も仏もない世界観に対する議論は
さんざんされて、結局一部の狂信的な科学信奉者以外
受け入れてはいない。ニュートンに代わってアインシュタイン
がもてはやされる理由はこのあたりにもある模様。
193:１３２人目の素数さん
05/12/23 09:07:34
人間にとって有益な定理は複数の命題から単純な命題を導き出すからコンピューターの糞定理からそんな形式を抜き出せば
比較的簡単に見付かる。
194:１３２人目の素数さん
05/12/23 09:09:49
>>189
修正。「記号論理の原理」じゃなくて「記号論理の効用」
原理は別にある。
>>191
そう言う次元の話じゃないの。「記号論理の原理」について
１０冊ぐらいの本で１０ヶ月ぐらいかけて考えてくれ。留年
覚悟で。尤も、本人に時期が来てないなら、それでも分らん
だろうが。
分らなくてもいい。走りの原理が分らなくても走れれば
素晴らしいから。
195:１３２人目の素数さん
05/12/23 09:11:12
無理数の話
＞URLﾘﾝｸ(www.gakushuin.ac.jp)
>>192
＞ニュートン力学の神も仏もない世界観に対する議論は
＞さんざんされて、結局一部の狂信的な科学信奉者以外
＞受け入れてはいない。
世界観は兎も角としてニュートン力学自体は受け入れているんでしょ
アインシュタインは別にニュートン力学が根本的に間違っていることを示したんじゃなくて
エネルギーが高い場合に出来る誤差を修正した、と考えるべき
大体科学と言ったって、究極的には、そう考えるのが最も尤もらしい、という以外の
根拠なんて無いんですよ
実験環境を整えてある実験をしたところ99回とも同じ、面白い結果が出た
で、100回目に同じことをしたら、やはり同じ結果が出るだろう、と推測するのが科学
いや、そうとは限らない、と考えるのが哲学
196:１３２人目の素数さん
05/12/23 09:12:50
数学は？
197:１３２人目の素数さん
05/12/23 09:15:08
？
198:１３２人目の素数さん
05/12/23 09:20:28
>実験環境を整えてある実験をしたところ99回とも同じ、面白い結果が出た
同じ実験をして違う結果がでると実験屋さんたちは認めないんでしょ。
数学の反例みたいなもんで。現実はわからんのをいいことに捏造なんか
もあるかもしらんが。
199:１３２人目の素数さん
05/12/23 09:38:51
2^(1/2)
うわっ
コンピュータ上で無理数を表しちゃったよ。どうしよう
200:１３２人目の素数さん
05/12/23 09:42:04
>>198
意味が分からん
理論屋さんでも同じ環境で違う結果が出るのを認めるのは量子論くらいじゃないかな
201:１３２人目の素数さん
05/12/23 11:44:31
>>199
皮肉なのかマジなのかわからん。
計算可能な実数と不可能な実数があって、ルート２は計算可能だそうだ。
いずれにしてもこのスレの本筋からずれている話だとは思うが。
202:１３２人目の素数さん
05/12/23 11:48:15
計算不可能な実数についての議論でさえ、
論理的な議論なら、記号論理に乗せられて、
コンピュータに乗せられるだろう。
203:１３２人目の素数さん
05/12/23 13:20:34
＞計算可能な実数と不可能な実数
計算可能ってどういう定義？
そういえば計算可能解析学とかあったね
かなりマイナーな分野だけど鴨さんとかそっち系の分野だったはず
204:１３２人目の素数さん
05/12/23 22:28:15
＞計算可能な実数
コーシー列の中でアルゴリズムが定義可能なものの集合、
なんちゃってそんな安直なモノのわけないね（＾＾）
でもいかにも数学界から相手にされない分野という感じだね。
205:１３２人目の素数さん
05/12/23 22:50:40
>>201,202
「計算不可能」を「計算可能でない」に直したい。
206:１３２人目の素数さん
05/12/23 22:53:35
遅い！
207:１３２人目の素数さん
05/12/23 23:07:22
一つの実数が誕生したと見るためには、
その実数の定義が、有限の長さの、意味の
はっきりした文または式によって記述されて、
しかも、その記述に基いて、その実数の
数値を、任意の精度で有限時間内に算出できる
ことが最低限必要なのだそうだ。
すると、そういう実数は可算個しかないのだ
そうだ。
円周率も、自然対数の底eも、ルート２も、
計算可能な実数であって、確実に「有る」と
言える数なのだと。
208:１３２人目の素数さん
05/12/23 23:16:44
このスレに燃えそうな人と普通の数学屋との間に言葉が
行き交うには、このあたり（チューリングの計算可能な
実数とか）を連結器にするしかないか。いずれの人に
とっても、最大の関心事というわけではないだろうが。
209:１３２人目の素数さん
05/12/24 06:04:25
整数部分をa(0)、n桁目の数字をa(n)としたときに
a(n)が計算可能函数（つまり全域再帰函数でいいんだっけ？）
となること、というのが定義か
でもそういう実数は計算可能というより定義可能とでも行った方が良いんじゃない？
210:１３２人目の素数さん
05/12/24 11:34:05
全ての計算可能でない実数を同一のプログラムで扱うことはできないのは自明だけど
そもそも計算不可能な命題がある事も自明なんだから特に問題はないとおもう
211:１３２人目の素数さん
05/12/24 11:40:02
あれだ。新しい定理の導出は出来るとして
導出できた定理が現在の学会の流行り廃りを考慮した上で価値のある定理かどうかを
AIが判断するのは無理があるだろうな
212:１３２人目の素数さん
05/12/31 19:55:39
世間に媚びる、あるいは相手を持ち上げてその気にさせる、
色仕掛けを使う、おべんちゃらを言う、
こういった知性がAIに備わり、孫氏などの計略をも学べば
危うからず。
213:１３２人目の素数さん
06/01/02 05:35:17
890
214:１３２人目の素数さん
06/01/05 21:47:52
自動証明ソフトが吐き出した証明が１ギガバイトにもなっていたら、
どうやってそれを読んで理解し納得できるというのだろうか？
215:１３２人目の素数さん
06/01/05 21:55:44
四色問題の時にコンピュータで解かせた時にも膨大な結果になったんだよな。
今から２５年以上前か…。
216:１３２人目の素数さん
06/01/05 21:56:47
数学者の本源直観によって霊視するのでつ。
217:１３２人目の素数さん
06/01/08 03:41:06
>>192
ゲーデルも、真理に到達するには科学的世界観だけではダメで、神学的世界観も
必要だと考えていたらしい。
来世は存在する。来世が存在しないとしたら今いるこの世界にも意味がないのだそうだ。
この本に書かれていた。
URLﾘﾝｸ(bookweb.kinokuniya.co.jp)
218:１３２人目の素数さん
06/01/08 13:40:16
「世界に意味がある」ってなんだろう
219:１３２人目の素数さん
06/01/09 00:46:35
>>217
ゲーデルの考え。
ゲーデル 竹内外史著 日本評論社
pp.178-179
もしこの世界が理性をもって構成されており、意味をもっているとするならば、
来世の再会は存在するにちがいありません。なぜならば、自分自身の発展および
人々との関係に無限の可能性をもっていながら、その千分の一も達成できない
人間という存在を創るということに、いったい何の意味があるでしょうか。
それはちょうど細心の注意と莫大な費用をかけて家の基礎を作り、それからそれを
無駄にしてしまうようなものです。しかし、この世界が理性をもって構成されていると
信ずる理由があるでしょうか？ 私はあると信じます。なぜならば、この世界は決して
混乱したものではなく、またどうでもよいというものでもなく、自然科学が示している
ように、いたるところに整然とした秩序があります。秩序というのはまさしく理性の
一つの形態です。
p.183
私は宗教のなかには一般に信じられているよりはるかに多くの理性があると信じています。
もっとも教会のなかにはありませんが。しかしわれわれは若いときから、学校で、
悪い宗教教育によって、また本や経験によって、そうでないと偏見をもつように教育
されています。
220:219
06/01/09 00:51:20
>>217
p.184
われわれは来世ではこの世での経験を覚えている。実は来世までは本当にその経験の
意味は理解していない。したがってわれわれのこの世での経験は来世で学ぶための
素材にすぎない。
p.185
もし、この世の経験を来世で覚えていることは不可能だという反対があっても、来世では
潜在した記憶をもって生まれてくる可能性があるということができます。その上、来世では
われわれの心の状態は現世よりはるかによく、したがって来世では、主要なことのすべてを
2×2＝4のように絶対に誤らない正確なこととして認識するだろうということを仮定しな
ければなりません。
pp.188-189
私が神学的世界像と呼ぶものは、世界とその内のすべてのものが意味と理性をもっている、
そして正しい疑問の余地のない意味をもっている、という思想です。そしてこの考えは
ただちに次の結論に導きます。われわれのこの世での存在はそれ自身きわめて疑問のある
意味をもっているにすぎないから、それは来世の目的のための手段でしかあり得ない。
さて、この世のすべてのものは意味をもっているという思想は、すべてのものはその原因
をもっているという原理と正確に対応するものです。そしてこの後者の原理はすべての
科学の基礎となっているものです。
221:219
06/01/09 00:58:04
>>219-220
竹内氏のコメント
p.178
ここに出てくるゲーデルは私のよく知らないゲーデルである。しかしこれもゲーデルの
一面である。神学や哲学でのゲーデルの考えは私などには分かりかねるが、それでも
彼の数学での考え方といろいろなつながりが認められる。
222:１３２人目の素数さん
06/01/10 00:20:54
ある記号系と公理系を仮定した場合に、
命題Mの証明が可能であるならば、そのような証明のうちで最も
記述が短い証明が存在する。この長さをL(M)としよう。
もしも、ある命題M1に対してその証明があったとして、
仮にその最短な証明の長さL(M1)が10＾100とかであったならば、
そのような命題は現実的には書き下すことが出来ないし
（なぜなら宇宙の原子の個数を越えている）、もちろん読み通す
こともできないであろう。10＾100ほどではなくても10＾10であっても
相当に困難であるが、計算機の容量と速度を持ってすれば格納したり
スキャンしたりすることは可能である。
223:１３２人目の素数さん
06/01/10 00:25:56
逆に云えば、証明が個人の手によるものであるとし、それの理解と確認も
各人が個人として行わねばならないとしたら、L(M)が比較的小さいような
命題Mしか（一生をかけるとしても）現実問題としては取り扱うことが
出来ないのである。一人でやるという立場を放棄して、１００人の集団で
分担して証明を書いたり、チェックする、そうしてトップダウン的に
証明のプロセスを分解して部分に分けて、、、と系統的証明が行えるならば
（証明の記述長は幾分長くなるかもしれないが）100人力となり、100倍長い
証明もあるいは検証できるようになるかもしれない、また１万人でなら
１万人力になるかもしれない。しかし人数が増えると次第に誤りが混入する
リスクが高まるので、独立な複数のグループに並行的に検査させたりするほか
本当にチェック機能が働いているかあるいはメクラ判を押していたりしないか
を確かめるためには、わざと証明の一部に誤謬を混入させてそれを検出するか
どうかを二重盲検検査する必要があるだろう。証明行為の過程自身の誤動作
を問題としなければならないからだ。
224:１３２人目の素数さん
06/01/10 00:46:42
そのようなことをしてもせいぜい1000倍とか１万倍とかしか規模を拡大する
ことはできないだろう。さらに数世代に渡って証明を検証するということが
考えられる、代々証明に取り組んで１０世代前から取り組んだ検証がまもなく
終わろうとしている、、、、というような具合にだ。
だが、やはり10＾100程度のところに限界があるに違いない。
全数検査しかないような問題であれば、10＾100はおろか10＾10000のような
問題であっても容易に作れる。
このような有限行為の立場からは、命題とは何か、証明とは何か、という
疑問が沸いてくる。
225:１３２人目の素数さん
06/01/10 00:56:11
>222
記号系というのは、命題にあわせて拡張されるもので、L(M)のような
関数は大した意味を持たないのではないか。
実際、複雑な数学を多くの人が理解できるようになったのは、記号の
整備によるところが大きいわけだし。
226:１３２人目の素数さん
06/01/10 02:39:20
コンピューターの自動証明を正当化する定理は誰が証明するのだ？
227:１３２人目の素数さん
06/01/10 02:52:21
>>224
先祖が姉歯秀次
228:１３２人目の素数さん
06/01/10 07:58:36
定理の自動証明って
１｡恒真式の生成
２｡論理変数と事象の結びつけ
に帰着するのでは、、
229:１３２人目の素数さん
06/01/13 03:01:31
素朴な疑問
自動証明をするためには少なくとも体系が決められていなければならない（言語や公理など）。
しかし、数学者はしばしば、新しい対象扱うために、それまで存在しなかった
新しい体系を導入して、そこで考える。そういう体系自体を新たに定義するような行為
は人間にしか出来ないのではないか？
230:１３２人目の素数さん
06/01/13 05:06:14
何でそう思うの？
231:１３２人目の素数さん
06/01/13 12:45:06
ゲーデル&タルスキーによって、次のことが
証明されています：
いかなる数学的問題でも
機械的計算で解決できるような
コンピュータ-プログラムは、
作れない。
232:１３２人目の素数さん
06/01/13 13:33:41
機械的計算じゃない何かをコンピュータに取り入れればできるかもしれない。
233:１３２人目の素数さん
06/01/13 13:59:41
機械的計算しかできないのがコンピュータの特徴付けでは？
234:１３２人目の素数さん
06/01/13 14:08:14
>>230
自動証明が出来るためには（たとえそれが”全て”の証明を網羅できないにしても）
まず体系自体を一つ与える必要がある。
体系を与えればその体系内で成り立つ可算個ぐらいの証明を
自動的に得ることが出来る。
しかし、どう考えてもその課程で、新たな
数学的に興味のある体系そのものが自動的に出てくることは
考えられない。
235:１３２人目の素数さん
06/01/13 14:25:14
>>231
いかなる数学的問題でも解決できる数学者が存在するわけではないし。
236:１３２人目の素数さん
06/01/13 14:52:28
>>234
Aを行う者にBを行うことはできそうもないので、Bを行う者は存在しない?
電卓ソフトで文書作成はできそうもないので、文書作成をするためのソフトは存在しない、とか。
237:１３２人目の素数さん
06/01/13 15:17:20
２３１のコメントの出自を明らかにしておきます：
文献：前原昭二『数学基礎論入門』朝倉書店
また、ゲーデルの不完全性定理に関するスレッドにも、
関連するコメントがあります。
238:１３２人目の素数さん
06/01/13 15:29:46
文献読むつもりはないが、「いかなる数学的問題」ってのは欲張りすぎ、ってか意味不明だな
239:１３２人目の素数さん
06/01/13 15:39:33
>>２３８
厳密さを欠いていて申し訳ないです。
『数学的に記述できる問題』
と言い換えればわかりますか？
もっと正確な説明が必要な場合、
やはり不完全性定理を勉強する必要があります。
ここでは長くなりすぎて説明し切れませんので。
240:１３２人目の素数さん
06/01/13 18:35:07
自動証明研究してる人は全員不完全性定理知ってるよ
不動点結合子とか停止性問題とか小テストで出るような基本中の基本だからね
だから誰も「全ての問題の解の列挙」なんて目指してないよ
241:１３２人目の素数さん
06/01/13 21:05:30
例えば代数学の基本定理を証明するために
自然に複素解析の定理を証明するようなコンピューターは作れるのか
242:１３２人目の素数さん
06/01/13 21:44:58
作れない。未定義要素全組み合わせを超える公理系
は作れない。サイコロを振って７の目が出ないことを
証明するようなものだ。
243:１３２人目の素数さん
06/01/14 04:50:28
ちょwwサイコロの例は例えが悪すぎる。
そんなのサイコロを上手く定義して、6つの場合に場合分けして考えれば
証明できるんでは？
244:１３２人目の素数さん
06/01/14 12:18:41
ＺＦＣとかの形式体系における証明に書き直せる証明は
時間が無限にあれば絶対に見つけられるよ。
リウビルの定理を用いた基本定理の証明も当然できる。
効率よく見つける方法は分野の相違に関係なく難しい。
計算機は分野の認識なんかしない。（させようとしなければ）
245:１３２人目の素数さん
06/01/14 13:37:05
＞＞244
自然数を含む命題論理の成否を決定するアルゴリズムは存在しない。
246:１３２人目の素数さん
06/01/14 16:34:18
>>236
○○作成ソフトの○○が１００年後に発見される概念だったら
現時点で○○作成ソフトは作れない。そして○○を発見するという
仕事が数学者に残される。その様な○○はいくらでもありそうなので
数学者の仕事はなくならない、・・・というはなし
247:１３２人目の素数さん
06/01/14 17:34:43
>>246
コンピュータに新しい概念を発見することはできないと思う理由は?
発見できそうもないと>>246が思うから発見できるはずがない?
248:１３２人目の素数さん
06/01/14 19:16:18
>>245
>>244 は定理の集合が帰納的可算だってことを言ってるだけじゃないの？
249:１３２人目の素数さん
06/01/14 20:44:00
新しい概念つってもでてくるのは数字だろ？
それって新しい概念だって人間が見て判断できることなのかね
250:１３２人目の素数さん
06/01/14 21:18:32
>>247
数学的に価値のある体系自体の数え上げが可能ということですか？
そうなると本当に、数学者要らないですね。”独創的”なんていう概念も意味がないことになるし、・・・
251:１３２人目の素数さん
06/01/14 21:23:30
>>つづき
体系そのものをコーディングして（何らかの数を対応ずけて）
数学的に価値ありという概念を式で表して、（これは矛盾しなければ価値ありとしていいのかどうかは良く分からないけど・・・）
その様な数の全体が計算可能かどうかを考えればいいのかな・・・
・・・まあ、どっちの結果にしろ自明じゃないことは分かるわｗ
252:１３２人目の素数さん
06/01/14 21:26:34
飛行機あるから電車は要らないですね
253:１３２人目の素数さん
06/01/15 16:51:59
有用な定理はこうやって作ると示したとたんに有用ではなくなる不思議。
254:１３２人目の素数さん
06/01/16 10:58:00
『自動証明』の研究では、今、
何が目的ですか？
詳しい人、いらっしゃいましたら、
ご回答願います。
私が少し興味を引かれる問題は、
公理系や取り扱う論理式の全体に、
どのような制約を設ければ、
任意に与えられた論理式が証明可能か
不可能かを機械的に判定できる
アルゴリズムを作れるか？
という問題です。
（興味のない人、ごめんなさいね～）
255:１３２人目の素数さん
06/01/16 11:04:33
>>219
地球上の人口が増えていくのはどう説明してるんだろう。
256:１３２人目の素数さん
06/01/16 14:28:11
>>255
「人は死んだら生まれかわる」と「人はみな、過去に死んだ人の生まれかわりである」が
違うことは理解しているか?
ついでに言っておくと、ゲーデルは来世が未来の地球だとも未来の"この世"だとも
書いてないよ。
257:１３２人目の素数さん
06/01/16 15:00:40
>>256
とすると、人間には２種類いることになるのか。
生まれかわりとそうでないもの。
不公平だなｗ
>ついでに言っておくと、ゲーデルは来世が未来の地球だとも未来の"この世"だとも
書いてないよ。
書いてないけど文脈からそうとしか思えない。
258:１３２人目の素数さん
06/01/16 15:36:54
来世は人大杉だな
259:１３２人目の素数さん
06/01/16 16:46:25
仮に我々が生まれ変わりだとしても前世の記憶がないっていうのは
致命的だな。これじゃ生まれ変わりだろうがそうでないだろうが
実質同じこと。
260:１３２人目の素数さん
06/01/16 18:05:57
そこで江原さんですよ
261:１３２人目の素数さん
06/01/16 22:38:27
過去に同じ遺伝子構造を持っていた人間が存在した場合に生まれ変わりとなる
262:１３２人目の素数さん
06/01/17 09:00:51
一卵性の双子の兄は俺と同じ遺伝子構造を持っているのだが
俺は兄の生まれ変わりなのか
あと、クローン人間禁止されたら俺は殺されるのか
263:１３２人目の素数さん
06/01/19 03:46:05
>>245
自然数があるのに命題論理とは・・・。
248の言うとおり、ＲＥだと言っているだけだよ。
いい加減な知識に基づいて考えるのは危険だよ。
264:１３２人目の素数さん
06/01/22 03:41:20
>>263
OMOIKOMI NO HAGESHII YATSUYONOO
265:１３２人目の素数さん
06/01/22 22:57:18
age
266:１３２人目の素数さん
06/01/23 22:48:57
>>264
仰るとおり。ごめん。２４４は誤り。
267:１３２人目の素数さん
06/01/24 09:42:34
coqとか使ってる？
268:１３２人目の素数さん
06/01/29 05:19:47
この手の問題の解決の糸口になりうるものは、
近年再び盛んになった人間の脳の機能や構造の研究であろう。
数学を行う作業を、脳の活動をリアルタイムでモニタリングする
帽子をかぶりながら、知的作業に対して脳が如何に使われるかを研究
するのである。おそらく、代数学と幾何学では使われる部位が
違っているとか、そういう類の発見とか、あるいはある事柄
を抽象化したり一般化したりする脳の機能の解明の糸口が
みつかるかもしれない。さらに、頭蓋を外してここだとめぼしを
つけた部位に電極をさして、。。。。。
そのようにして、脳の推論する機能が段々よく分かってきたら、
あるとき偉大な者が現われて、脳シミュレータを開発し、ついに
プログラムによらない自己学習型、自己発見型、自己推論型の
人工数学者ができるかもしれない。彼は外界の情報をネットと
電子ライブラリーを参照しながら、ただもくもくと数学にいそしむ
のである。世間はこのシステムの完成をみて、もはや数学者は要らない
と短絡的な意見に走り、数学者を野に放って数学以外の労働を
強制するかもしれない….
269:１３２人目の素数さん
06/02/05 07:27:08
281
270:１３２人目の素数さん
06/03/02 16:59:59
367
271:中川泰秀 ◆IvNr9.tOCg
06/03/13 16:40:57
数学が正しい事を自動で証明して見よ
272:１３２人目の素数さん
06/03/14 04:35:18
age
273:１３２人目の素数さん
06/03/14 14:46:41
コンピュータは自分自身が正しいことを証明できない。
証明しようとすると、必ず自己矛盾か無限ループに落ちるから
考えないようにしている。自己のことを考察した瞬間に
システムのどこかに必ず不動点が生じて、そこで引っかかって
抜けて来れなくなるのだ。
274:中川秀泰 ◆IPeKUwqiHM
06/03/14 14:50:55
仲々良い所を付いているじゃないか
これはコンピューターばかりでなく人間にも当てはまる。
275:BW of Tama King
06/03/14 14:54:52
>>274 キングに証明させるのがよかろう。
奴は数学の召喚獣スクリプトだから。 普通あんなけレス出来んぞ。
キング無理すんなよー オーバーヒートするぞぉー
276:GiantLeaves ◆6fN.Sojv5w
06/03/14 15:00:04
talk:>>275 私を呼んだか？
277:BW of Tama King
06/03/14 15:01:30
>>276 呼んだよ？ 数学が正しい事を自動で証明して見よ だって。
278:中川秀泰 ◆IPeKUwqiHM
06/03/14 15:07:02
◆6fN.Sojv5w
等というking見た事無し
279:GiantLeaves ◆6fN.Sojv5w
06/03/14 15:36:00
talk:>>277 では数学とはどのような命題か？
talk:>>278 何だよ？
280:BW of Tama King
06/03/14 15:45:12
>>279 中川さんに聞け。
281:１３２人目の素数さん
06/03/26 14:29:19
282:１３２人目の素数さん
06/04/04 22:11:13
このスレもう終わりか？
283:１３２人目の素数さん
06/04/15 23:09:20
193
284:中川秀泰
06/05/12 05:31:36
どうせ哲厨のスレだから終わりにして良い
285:１３２人目の素数さん
06/05/13 22:25:06
521
286:１３２人目の素数さん
06/05/14 05:01:34
どうせなら形式化された証明のデータベースの話とかしたいな。
287:１３２人目の素数さん
06/05/16 15:42:02
MIZAR!
288:１３２人目の素数さん
06/05/16 16:04:34
定理の自動証明ってMathematicaとPrologで既に商品化されてるよな
289:１３２人目の素数さん
06/05/26 14:14:49
620
290:１３２人目の素数さん
06/06/16 01:05:04
912
291:１３２人目の素数さん
06/07/28 15:37:13
977
292:１３２人目の素数さん
06/08/15 04:09:52
あ あ あ あ あ あああああ
あ あ あ ああ あ あ あ
あ あ あ あ あ あ あ
ああ あ あ あ あ あ あああああ
あ あ あ あ あ あ あ あ
あ あ あ あ ああ あああああああ
あ あ あ あ あ あ
あ あ
あ あああああ
あ ああああああ
あ あ ああ あ
あ あ あああ ああああ
あ あ あ あ あ あ
ああああ あ あ
293:KingOfUniverse ◆667la1PjK2
06/08/17 06:00:12
talk:>>292 人の脳を読む能力を悪用する奴を潰せ。
人の脳を読む能力を悪用する奴を潰せ。
294:１３２人目の素数さん
06/08/30 16:55:54
648
295:１３２人目の素数さん
06/10/03 00:21:38
174
296:１３２人目の素数さん
06/11/12 23:47:29
968
297:１３２人目の素数さん
06/12/07 20:24:25
自動証明の研究に、何の価値があるの？
298:１３２人目の素数さん
06/12/07 20:38:28
>>297
なぜ出来ないか考えるきっかけになる。
299:１３２人目の素数さん
06/12/07 20:52:47
こらっつぐらいからやれば何がネックかわかるよ。
300:１３２人目の素数さん
06/12/07 21:30:46
こらっつって３ｘ＋１と．５ｘをコンフォーマルマップで２つの
円のあいだの領域に飛ばして、グラフが１に収束する力学系を
つくればいいんでしょ？
301:数学系のD1です
06/12/07 21:43:09
>299
ありがとうです
302:１３２人目の素数さん
06/12/07 23:13:55
f(z)=arg(z-p0)e^2π(1/(1+1/|z-p0|))i
は直線を同心円にマッピングする。
303:１３２人目の素数さん
06/12/07 23:41:34
f(z)=arg(z-p0)e^2π(1-1/(1+|z-p0|))i
は直線を同心円にマッピングする。
304:１３２人目の素数さん
06/12/07 23:42:34
こらっ
305:１３２人目の素数さん
07/01/01 00:05:23
↓うるせーんだよ
↓このスレを見ている人はこんなスレも見ています。(ver 0.20)
306:１３２人目の素数さん
07/02/05 17:08:31
610
307:１３２人目の素数さん
07/02/07 04:18:00
それより証明を形式的に記述して検証する方法に興味がある
308:１３２人目の素数さん
07/02/07 05:05:15
思考とは組合せ探索なり。
309:１３２人目の素数さん
07/02/07 11:50:21
コンピュータで数万年かかるような組み合わせから
最適（に近いもの）を一瞬で見つけられるのはなぜなんだぜ？
310:１３２人目の素数さん
07/02/07 21:31:58
きっと将棋のプロと同じ原理だよ
311:１３２人目の素数さん
07/02/08 06:28:03
>>309
逆もあるよん
312:１３２人目の素数さん
07/02/10 18:55:12
人間の場合超自然的な予見ができるから
313:１３２人目の素数さん
07/02/11 13:27:43
人はそれを「当てずっぽう」と呼ぶ。
314:１３２人目の素数さん
07/03/11 17:58:47
age
315:１３２人目の素数さん
07/03/15 23:25:07
結局こういうことなんだよ
人間も全数探索に近いことをするけど、
コンピュータより早く終わらせられるのは、
その先に答えがあるかどうか評価する能力の違いなんだよ
ゲーム木を育てるジョウロだけじゃなくて、その枝を刈る鋏も重要なんだよ。
ようするに翠s
316:１３２人目の素数さん
07/03/16 00:59:14
>>307
有名なんで紹介するのも気が引けるんだけど、Coqっていうソフトやら、証明
を形式的に記述して検証するものっていろいろあるよね。
その手のソフトの下地の理論を探れば、検証する方法の勉強はできそうだが。
317:１３２人目の素数さん
07/03/16 04:06:48
>>316
プルーフチェッカのMizarってのをけっこういじったけど、
けっこう面白かった。
ただ言語仕様がどこにもはっきりと書いてなくて、(基本はpdfとかに書いてあった)
既存のライブラリを読んで自分で考えないといけなかった。
なんか基本は述語論理での推論法則だけを使ってやるって感じだったな
でも等式とかの導出を詳細に(両辺からxを引いたとか)書かないでも
成り立っててかつあんまり飛躍してなければ受理されたけど、
そのへんはどうなってるかわからなかった。
318: ◆WSu5GQQTQ2
07/06/05 12:06:21
数学者は子供が覚えられる段階の算数→数学の段階から
論理的にすっきりした証明を選び出せば十分なんじゃないかなー
自動証明は証明可能かどうか、あと数学自体が無矛盾じゃないか、
の判定だけでいいと思う。
319:１３２人目の素数さん
07/06/24 23:48:15
age
320:１３２人目の素数さん
07/06/25 00:28:07
＞証明可能かどうか、数学自体の無矛盾の判定
ほとんどの数学理論では、無理。
321:エレガントな解答を求む
07/06/25 00:40:34
つーか 例えば整数論なんて殆どパズルじゃん
heuristics を入れなきゃにっちもさっちもいかない
a! ha!なかんじは少なくともTuring Machineには無理だね
人間の脳を細胞レベル、分子レベル、素粒子レベル、、、で解明
できなければサル真似だよ
322:１３２人目の素数さん
07/06/25 13:43:13
背理法ってなんかツンデレっぽくね？
べっ、べつにa=bなんて言ってないわよっ！
ただ、a≠bだったとしたら、
あれがあーなったりこれがこーなったりして
いろいろムジュンするって、それだけなんだからっ！
323:１３２人目の素数さん
07/06/25 14:19:34
>>322
漏れは逆だと思う。
会うといつも笑顔で挨拶してはくれるが
二人きりで会おうとするとなぜかはぐらかされる。
だからあの笑顔は好意の証ではない。
324:１３２人目の素数さん
07/06/25 14:21:35
>>322
お年をめした准教授が
「ツンデレって、なんやねん？」
ツンドラ気候か？って…
325:１３２人目の素数さん
07/06/25 14:28:09
>>324
アニヲタには理解は早いかもしれないが
（アニメを知らない）准教授に説明するには
かえって困難だ
准教授の使っているパソコン（win95)みたいな性格のことですよ
と言っとけ
326:１３２人目の素数さん
07/06/25 14:31:15
うちの弟は、平野綾＝ラムちゃん、だと思ってた。
それは平野文で「ふみ」と読むんだが。
（実はついさっき知ったｗ）
327:１３２人目の素数さん
07/06/25 14:35:37
どうでもいいが
ガッキー＝ハルヒ キョン＝マツケン
で「憂鬱」実写映画化って、あれマジで無いのか。
長門＝ホマキ 古泉＝平岡祐太 あたりまで
俺の中ではキャスティングが出来上がってるんだが
みくるが・・・・
328:１３２人目の素数さん
07/06/25 14:48:33
>>322以降から
そろそろスレ違いっぽくなってきたな…
お前らアニメ板で語ってくれい
329:１３２人目の素数さん
07/06/25 15:51:51
>>327あたりからアニヲタじゃなく
アイドルヲタのニヨイもしてきたが
330:１３２人目の素数さん
07/06/25 18:48:12
ツンデレ教会は実在する
331:１３２人目の素数さん
07/07/01 14:51:58
コンピュータによる将棋やチェスなどの知見を、定理の自動証明に
も適用できるのではないだろうか。過去の証明を沢山放り込んで
パターンを学習させることで、未知の命題が試行錯誤により、より良く
解けたりしないかな。
特に、正しい命題の場合には、いってみれば詰め将棋のようなものだから、
どうだか分からない命題よりは易しいのではないだろうか？
332:１３２人目の素数さん
07/07/01 21:06:28
4色問題みたいに扱われるだけのような
333:１３２人目の素数さん
07/07/02 11:34:51
すべての組み合わせで成り立つ（あるいは成り立たない）ことを証明する場合と、
組み合わせの中からひとつでも成り立つ（成り立たない）ものを見つければよい場合は違うんじゃないかな。
334:１３２人目の素数さん
07/07/03 04:00:39
>特に、正しい命題の場合には、
正しいかどうかが、そもそもわからないから、
そこで「正しいかどうかの判定」で、苦労するのでは？
「正しい（＝証明可能）」なことがわかっているのであれば、
そもそも機械で証明図を探索する目的が半減すると思う。
335:１３２人目の素数さん
07/07/03 04:29:20
正しいとまず仮定して正しい命題用の思考を計算させる
そして偶然にも「正しい命題の場合」だったら、有用なわけだろ
336:１３２人目の素数さん
07/07/03 06:07:26
実は俺、そーゆープログラム作ろうかと思ってるんだよな。
準ウィキ方式で、わりと誰でも参加できるからデータ量けっこう楽に増えると思うし。
たとえばAはa1,a2,a3...といった性質を持ってて、Aであり、さらにbの性質を持つとBであるとか、まぁ完全な証明ができるわけじゃないけど道筋をたたき出す感じで。
A→Zを証明するとしたら、Aのa3の性質はZであるための絶対条件であるゆえにZとかを自動で叩き出す。
証明って今までに出された結果が効率的に使えてないから難しいと思うんだよね。だったらそこはコンピュータにやらせようと。
337:１３２人目の素数さん
07/07/03 09:20:57
絶対条件てなんだよ
338:１３２人目の素数さん
07/07/03 10:13:04
ゴメス十分条件
339:１３２人目の素数さん
07/07/03 11:00:19
>>331 データマインニング？
340:１３２人目の素数さん
07/07/03 11:10:04
>>336
ちょっと興味あるんだけど、その「性質」ってどういうデータ構造？
341:１３２人目の素数さん
07/07/07 06:13:46
>>336
おもしろそうですね。なるほど、自動証明って、
こういうことを研究するのですか。。
342:math太郎
07/07/07 06:45:59
>331
おれは将棋のプログラム作ったことあるよ。
弱いけどね。。。
結局のところ、探索をどこで打ち切るか？というのは速度の
問題でもあるが、つきつめれば盤面評価関数を
どのように作るかの問題なんだ。
盤面評価関数は、その盤面上の状況に数値を
あてはめて、得点をつけるわけだ。
それで得点の高いほうを選択するわけ。
数学の証明をそのように得点化して評価できるかというと、
多分、無理じゃないかな？
343:１３２人目の素数さん
07/07/07 08:57:21
>>342
なるほど。
数学の証明に適用するには、
まだまだハードルが高いんですね。
344:１３２人目の素数さん
07/07/07 09:00:12
数学の証明図の探索の場合は、
探索を途中て打ち切って得られた「証明図」が、
所要の命題に正しい証明を与えているか否かの判定も、
別に必要になりますね。
345:１３２人目の素数さん
07/07/07 09:05:45
ゲーデルの不完全性定理により、そもそも不可能では？
346:１３２人目の素数さん
07/07/07 09:07:56
>>336 が言ってるのは、証明探索とは別のアプローチかな？
証明を探索すると結果が出れば必ず正しいけど、なかなか現実的な時間では終わらない。
そこで結果の正しさをある程度犠牲にして計算量を削減しようと。
347:１３２人目の素数さん
07/07/07 09:11:48
つまり、理想としては、「正しい場合」には、
正しい証明図がでるまで探索を続けるのだけれど、
現実問題として、探索を途中で打ち切らなければならない。
そのとき得られた解を、
今度は正しい証明図を与えているかどうかの判定にかける
（ミザールみたいなコンピュータ・プログラムで）
・・・ということかな？
348:346
07/07/07 10:14:14
証明図の探索はやらずに、もうちょっと粗い評価をするのかな、と思った。
349:１３２人目の素数さん
07/07/07 13:34:41
先ずその定理が正しいことを証明すべきでは？正しいことがわかれば後はその具体的証明は稚戯に類すべきでは？高木先生の近世数学史談の正十七形の意見を参照。
350:１３２人目の素数さん
07/07/08 11:44:29
３４９追加 然るに、ゲーデルの不完全性定理によれば、すべて命題の正否をコンピュータ式に自動的に決定することは出来ない。
351:１３２人目の素数さん
07/07/08 22:53:30
10 for i=1 to ∞
20 if theorem=true print"QED"
30 next i
352:１３２人目の素数さん
07/07/09 00:44:43
ループ変数使われてねええ
353:１３２人目の素数さん
07/07/09 00:56:16
>>351
昭和のかほりがした
354:１３２人目の素数さん
07/07/09 01:07:48
BASICだったらthenが要るし
355:１３２人目の素数さん
07/07/09 12:17:39
そこは goto で無限ループだろ
356:１３２人目の素数さん
07/07/25 23:07:58
ゲンツェンシステム
357:１３２人目の素数さん
07/08/28 02:29:56
証明の検証だけでも十分便利だと思うけどね
358:１３２人目の素数さん
07/09/06 23:34:55
二年。
359:１３２人目の素数さん
07/10/30 12:31:59
747
360:１３２人目の素数さん
07/12/20 09:07:39
>>357
実用化すれば、レフリー要らなくなるよね
361:１３２人目の素数さん
07/12/20 15:10:56
コンピュータで検証できたらいいなと思うことはあるけど、
チェッカに渡す証明を書く手間考えるとやる気にならない
362:１３２人目の素数さん
07/12/20 15:46:56
コンピュータでできる事はせいぜいMathematicaでできている事ぐらいじゃないかと思うのは発想が貧困ですか
363:１３２人目の素数さん
07/12/20 16:55:29
>>361
お前さんは
メールを打つのが、手間かかるので
そのまま、電話をするタイプ？
364:１３２人目の素数さん
07/12/20 23:39:35
>>363
いや、電話はなんとなく嫌いなのでメールする
365:１３２人目の素数さん
07/12/21 13:25:21
>>362
貧乳だな
366:貧乳はステータスだ希少価値だ
07/12/22 05:38:17
ｒ､ _ .. ＞: : :ｿ`ｰ― ､}ﾉ ＿
_x≦メ_,-､ ,ｨ≦:_:.／:/ ;ｲi: : :j : : : :＼ {ヽ.__>､_ゝ
. ﾍﾆ ,ｨ r＜ ／:/:/:/ {:| : ∧ : ヽヽﾊ r―-､ ﾉ-ｧ.勹
／ィヽ| ﾄ'ノ / /.:| :{/＼ﾄ: :｣／Vﾊ:', } } ,ｱ / ｢`こﾍ
｀7_} /,イ: :| ﾊｚ== ヽ{ =弍 | |:| | ＜_へ＞ { ｆ=} }_
,-､_fﾍxー､ |: ∧ { ｰ'ｰ' ･}:jﾊ{:.′ __ﾍﾆｱ‐vｨｱﾄ､ヽ-'
. {／ヽﾉｲ¨ｰ' Ⅵ/: i＞ ､ _, ﾘ}│{ ﾍーｧ f ¨くtfｲ |
ｨ_／ |: :|/:.,ｨ=厂{≧': /:∨ /／ r=} ﾄ {__,ﾄ､
／}fﾆニﾍ |: :|ﾍ {¨7´ /: /＼:{ {ﾍ ＜八_＿ ﾉ
≦ｨくﾄrｆ}f,勹 rﾍ: |∧ |/, イ :/ ⌒} |_.} f{ ｨ=士ゝ
. |_}ﾍ-'¨ｰ' 人.ヽ{⌒{7＞.Ⅳ∧ /¨＞ 、ノ＾ﾆ勹 ヾ (f_ﾉｰ､
／}ｰ士= .ヘ `∧, 小、__} / : ｰｧ' ,ノ フ／ ´¨
≦ｨく }`{z} ＼ Ｙ_./ / { ∨:/´ ｨ く ｰｆﾆ勹
. |_}くニニﾍ / ヽ/∨}／｢￣{ｱ:ー' : : ﾍ ／,＜...
r-ﾉ7_ __{ヾ> ｰ≦.ｨ７/ /│ V ﾊﾍ : : : : : : ',≦ｆL ___fヾ>
ﾌ / ,ｲｰ'¨ く/// / :| ∨ﾊ ',: : : ｊ: : :ﾊ ｧ/ ｲｰ'¨´
{./ ゞこﾌ /// / | ∨ﾊﾊ: : :}Ｖ:}: |ﾑ{ ゞこﾌ
//7={...__ | __ ...},ｘ≦: :ﾉ |ﾉⅤ
367:１３２人目の素数さん
08/01/17 01:09:39
ねぇ、誰も言及してないっぽいから言っとくけど、チューリングマシンって乱数とか無いぢゃん？
個人的には量子論的な乱数の存在がゲーデルさん的な「人間はコンピュータよりつおい」の根源的原因かもと思うのさ。
でさ、時刻とかカーソルの動きとか様々な外部要因を取込んで強化したぎじ乱数を、ぎじでもいいから使うべきだと思う。
既に与えてある定理の一部の文字をランダムに取換とか改変し、その文が論理的に正しい文になるまで取換や改変、を続けさせるとか。
与えられた語彙の中からランダムに定義行為や公理設定行為を行わせてみるとか。
368:367
08/01/17 01:12:35
論理的に通じるかは毎回チェックさせてさ。i^2=-1、とかで実数から虚数へ拡張とか結構平気でやりそうな気がするさ。
膨大な汚い小定理や汚い定義の中から、他の小定理や定義からの引用回数が多い程優先度を上げて処理し、
つまり母定理母定義、ハブ定理ハブ定義として進化論的に自然淘汰させるとか。googleみたいな。そこで「ネットワーク理論」とか応用してみたり。
つまり、貧乳は本人が気にしているのも含めて良いのやから誇られたらぐんにょりやね、に一票。
369:１３２人目の素数さん
08/01/17 01:21:39
そんな擬似乱数で何かが変わるわけが無いがな
370:367
08/01/17 01:51:40
でもさ、ランダムにコピーミスしながら自己増殖するデータとかで「人工生命」という概念を確立した人もいるみたいだよ。計算力で膨大な世代を作れる上、寄生生物とか実際の生命の現象に似た現象が起きたりして色々面白いらしい。
人間が定理や定義の「善」をコンピュータにいちいち正すのは面倒。
というワケで～進化論的に目指させればそれなりにそこそこの結果でるんじゃないカナ～と思う。なるべく簡潔で汎用性の高いのが生き残ってゆくとかさ。
人間の理性的処理能力だってもともとは遺伝子のコピーミスというぎじ乱数から出たっぽいしさ。
371:１３２人目の素数さん
08/01/18 09:14:20
何をやりたいのかよく判らない．
自動証明したいの？数学の定理生成をしたいの？
新たな数学体系の構築をしたいの？
372:１３２人目の素数さん
08/01/19 00:02:37
>>106
ヒント【ゲーデルの不完全性定理】
373:１３２人目の素数さん
08/01/19 00:10:02
>>372
不完全性定理がどうしたって？
374:１３２人目の素数さん
08/01/24 22:52:06
>>370
その方針だと計算の効率とかには影響を与えるだろうから、
効率のいい（擬似）自動証明方法とかは思いついてくれるかもしれないが、
>>367で書いてるゲーデル的な意味での性能は一つも変わらない。
というか、ちゃんと勉強すれば簡単に分かることなんだけど、
例に挙げているような擬似乱数の類では
コンピュータの計算可能性そのものに関しては何も影響を及ぼさないぞ。
せいぜい計算量レベルの影響しかない。
375:１３２人目の素数さん
08/03/28 03:47:22
838
376:１３２人目の素数さん
08/05/05 22:47:32
425
377:１３２人目の素数さん
08/05/09 08:29:49
目的別で選ぶ定理証明器
1. 俺が書いた証明をチェックしたい → Proof Checker (Mizar)
2. 定理をあたえたら全自動で証明を返してほしい → Automatical Theorem Prover (Djinn, Mathematica)
3. 半自動で証明を手伝ってほしい → Proof Assistant (Coq, Isabell)
ただし、2.は扱える領域が極めて狭いので注意!! そして、証明できないときもある。
1.3.はすべての数学的命題を扱うことができるが、人間の努力も必要である。
378:１３２人目の素数さん
08/05/10 08:06:54
age
379:１３２人目の素数さん
08/05/10 08:43:13
>>377
2は、証明できない場合、フリーズしちゃうんですか？
380:１３２人目の素数さん
08/05/10 10:39:58
>>379
証明器によると思う。よく知らない。
ただ、計算量は指数的に膨れ上がる事が知られており、自動証明可能なものであっても、
現実的な時間内には終わらないこともある。
そもそも、自動証明では記述できる命題が限られるため、証明支援器 (377の3.)を用いて、
部分的に自動化する方法が最も現実的である。
381:１３２人目の素数さん
08/05/10 11:46:39
>>380
ありがとう。
382:１３２人目の素数さん
08/05/14 02:44:56
(ﾟДﾟ)≡ﾟдﾟ)、ｶｧｰ ﾍﾟｯ!!
383:１３２人目の素数さん
08/05/14 02:48:16
(ﾟДﾟ)≡ﾟдﾟ)、ｶｧｰ ﾍﾟｯ!!
384:１３２人目の素数さん
08/05/14 03:44:52
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
385:１３２人目の素数さん
08/05/14 10:30:25
(ﾟДﾟ)≡ﾟдﾟ)、ｶｧｰ ﾍﾟｯ!!
386:１３２人目の素数さん
08/05/14 11:37:11
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
387:１３２人目の素数さん
08/05/14 11:38:58
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
388:１３２人目の素数さん
08/05/14 11:39:28
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
389:１３２人目の素数さん
08/05/14 11:42:13
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
390:１３２人目の素数さん
08/05/14 11:47:46
１０００までやんねぇのかYO？
いくじなし＾＾
１０００までやんねぇのかYO？
いくじなし＾＾
391:１３２人目の素数さん
08/05/14 19:49:32
ん？もう終わりｗ
392:１３２人目の素数さん
08/05/15 21:42:44
>>320
> ＞証明可能かどうか、数学自体の無矛盾の判定
> ほとんどの数学理論では、無理。
無矛盾性の証明が無理なのでは無く、無矛盾な公理系の上での
すべての真な命題の証明が無理なのでは。
393:１３２人目の素数さん
08/05/15 23:37:58
僕は以前は形式的体系ということについて、色々思うことが
有ったのだが、この頃は、Frege構造というものについて気に
なってきたのだよ。フレーゲ構造って、なんか面白そうな予感
がする。
394:１３２人目の素数さん
08/05/16 07:34:11
>>393
フレーゲってよく知らないけど、普通のhigher order logicと何が違うの？
395:１３２人目の素数さん
08/05/27 22:29:39
AgdaとかCoqとかを勉強したいです。でも全然わからないです。おすすめの初心者向けの文献はありますか？
396:１３２人目の素数さん
08/05/28 07:16:42
Lectures on the CurryHoward isomorphism
URLﾘﾝｸ(citeseer.ist.psu.edu)
397:１３２人目の素数さん
08/06/28 17:11:46
未来言語Agda
URLﾘﾝｸ(d.hatena.ne.jp)
398:１３２人目の素数さん
08/07/05 10:44:38
age
399:１３２人目の素数さん
08/07/29 11:26:01
最近集合論を形式化したノート作ったんだけど、せっかくだからプルーフチェッカーにでも通して遊んで
みたいんだけど、個人的に遊べるソフトはどれがお勧めですか？
今、MIZARとか言うのを解読中なんですが、HIDDEN.VOCが見当たらないんだよねえ。関数記号とかも
自分で定義したいんだけど、そういうのはＭＩＺＡＲには向いてないのかなあ。
もっとグラフィカルでわかりやすいのがあるといいなあ。
400:399
08/07/29 11:34:37
もしかして>>377ですべてなのかな。そうだったらごめん。
401:１３２人目の素数さん
08/08/01 08:48:26
>>399グラフィカルってのは現状むずかしいんじゃないかなぁ。
それより、そのノートを公開すれば、いろんな人が各ツールで実装してくれんじゃね？
それをグラフィカルに眺めればok
402:１３２人目の素数さん
08/08/19 07:41:45
age
403:１３２人目の素数さん
08/08/26 04:40:30
「全ての命題を自動証明することは出来ない」は必ずしも
「ほとんど全ての命題を自動証明することは出来ない」を意味しない。
もしかすると、
「ごく一部の命題（測度０笑）を自動証明することは出来ない」なのかも
しれない。
また、「正しいと証明できる命題であっても自動証明することは出来ない」
を意味しないことに注意。
ある一つのパターンの命題（証明不能の証明に出てきたようなタイプの
命題）だけが、証明不可能であるだけなのかもしれないのだ。
404:１３２人目の素数さん
08/08/26 15:11:17
くだらん妄想膨らます暇あったら本読めよ。
405:１３２人目の素数さん
08/08/27 05:35:12
初等幾何に限定すれば定理の自動証明はある程度上手くいったりしないかな
補助線引いていくだけだったりするし
406:１３２人目の素数さん
08/08/27 13:47:02
>>405
無理でしょうな。平面幾何の定理は非常に多くあるし、その証明は難しい。
よって機械的に証明を探索しても計算量が爆発してオワリ。
407:１３２人目の素数さん
08/09/03 15:25:07
よくＴＶか雑誌などに、詰将棋３～５手詰なんかあるじゃん
あれって、過去に出された（既出）な問題ってのもあるのかな？ってふと思った
とあるマニアな人間が、過去（１世紀以上も）の詰将棋問題を
データーベースみたいなものに、インプットしてて
例えば今週出題された、詰将棋問題を、そのデーターベースで"検索"したら
ヒットして、19xx年xx月xx日 読＠新聞 にて、同問題がありました とかね
ｳﾝ十年前のNHKで、将棋の特番だったかうろ覚えだが
詰将棋などではなく、実際の戦いの局面の配置を、コンピュータでインプットして"検索"し
同局面が、過去に3度ありました。と出て、先手後手どちらがその後有利または勝ち負けなのかなどの
判定らしきものが、あった。
408:１３２人目の素数さん
08/09/03 15:44:56
ウン十年前はさすがにないでしょ
たぶん数年前の順位戦A級最終日の中継で勝又5段（当時）がデータベース使ってたときの事だと思うけど
409:407
08/09/03 16:29:55
>>408
ウン十年前ではなくて、十ｳﾝ年前か
羽生さんが、全盛期の頃
（今でも、健在ですが・・・）
これと似たようなもんでさ
高校教諭が相加相乗平均に新証明法
URLﾘﾝｸ(www.asahi.com)
この相加相乗平均の証明方法は５０以上あると
それらをデーターベース化して、証明の"判定"みたいなものを作れないかな？
「この証明方法に気づいた人はこれまでにもいたはず。
簡単すぎるので発表済みと思ったのかもしれない」
既出な証明であった or 新証明である とかね
そしてこのような判定プログラムを一般人の人でも、扱えるシステムを設けるとかね
410:１３２人目の素数さん
08/09/03 16:40:00
YASUHARU UCHIDA (Kurashiki Kojyoike High School)
A SIMPLE PROOF OF THE GEOMETRIC-ARITHMETIC MEAN INEQUALITY
URLﾘﾝｸ(www.emis.ams.org)
411:１３２人目の素数さん
08/09/06 23:35:12
三年。
412:１３２人目の素数さん
08/09/17 09:30:27
>407
遅レスですが「詰め将棋データベース」はもちろん存在します。
但し、有償でかなり高価なものらしく（セット全体で10万円くらい？）
Web上などで誰もが検索や同不同チェックができるようにはなっていないようです。
413:１３２人目の素数さん
08/09/17 12:08:18
>>412
参考になりました。ありがとうございます。
詰め将棋データベースの同局面検索機能みたいな感じで
それを数学に使えないかなってね。
例えば、大学入試問題。
大学側が、いろいろ問題を考えて作る。
しかし過去にどこかの大学で似たような問題（または、全く同じ問題）があったらマズイよね
そのような検索機能があったら便利かなってね。
実際は、人間たち（教授・准教授その他）が、案外手作業で探っているのかもしれないｗ
過去問題集（赤本）とか引っ張り出してね。
事実、国語の分野では、煮詰まっているらしく
過去の問題を使いまわしを認めるかどうか検討しているらしい
（それは、著作権などの問題があるので、円滑には進まないとか）
414:１３２人目の素数さん
08/09/18 00:41:41
age
415:１３２人目の素数さん
08/09/18 13:38:21
コンピュータでトレミーの定理の自動証明に成功した
416:１３２人目の素数さん
08/09/18 14:48:13
凶悪的に強いチェスソフトを教えてくれさい
417:１３２人目の素数さん
08/09/18 21:40:13
>>415
アルゴリズムうｐ
418:１３２人目の素数さん
08/09/29 11:11:26
Mizarって言う定理証明支援システムがあるの知ってる？
その言語で数学の論文書くと証明をチェックしてくれるんだってさ。
いまそれでチェック済みの論文がデータベース化されていて、
そこで既に証明済みの定理も新しい定理の証明に使用できてそれをまたチェックできるんだって。
URLﾘﾝｸ(www.cs.ru.nl)
ただしその言語での論文は通常の4倍くらいの長さになるそうな。
419:１３２人目の素数さん
08/09/29 11:58:17
>>418
Mizar自体は激概ではあるが、しかし僅か4倍で済むというのは意外だった。
420:１３２人目の素数さん
08/09/30 06:14:42
Mizarで書いた論文は普通の雑誌だと受理されるのかなと思ったが
労力的に絶対無理だから考えるだけ無駄か
421:１３２人目の素数さん
08/10/16 18:06:18
つーかMizarって、どんな言語を使っているの？
422:１３２人目の素数さん
08/10/25 15:20:26
age
423:１３２人目の素数さん
08/10/28 09:26:13
コンピュータは０と１、すなわち真か偽かの二種類。
数学はゲーデルの不完全性定理により真でも偽でもない命題がある。
だからコンピュータと数学は合わない。
真でも偽でもない命題をコンピュータにやらせたら
無限ループに陥る。
その場合は
if p<>true and p<>false then
exit sub
endif
と書くといい。
424:１３２人目の素数さん
08/10/28 20:26:04
わかってねえな
425:１３２人目の素数さん
08/11/03 12:00:34
わかってないな
426:１３２人目の素数さん
08/11/03 12:16:34
取り得る可能性が有限の場合はコンピューターはすべての可能性を実行して反例を探せばいい
すべてのパターンを実行しても反例が見つからなければ証明されたと言える
無限の場合は無理
427:１３２人目の素数さん
08/11/03 21:11:32
むかし第五世代というインチキなのがあったけど？
428:１３２人目の素数さん
08/11/03 21:40:24
クラウドコンピューテイングでゲーデル数解析マシンをつくればすべての定理は証明されてしまう。
429:１３２人目の素数さん
08/11/10 21:06:19
URLﾘﾝｸ(www.too.com)
紛らわしい名前のソフトがあった
430:１３２人目の素数さん
08/12/03 16:40:18
800
431:１３２人目の素数さん
09/01/03 09:07:39
>>428
そんなわけねーだろ
432:１３２人目の素数さん
09/01/03 18:49:58
そういえば数学板には数値解析のスレがないね
どっちかといえばシュミレーション板やプログラム板になるのかな
でも理論的なことを語るのに数学板にも一つぐらいあってもいいと思うんだが