2ちゃんねる ★スマホ版★ ■掲示板に戻る■ 全部 1- 最新50  

■ このスレッドは過去ログ倉庫に格納されています

コンピューターによる定理の自動証明

1 :132人目の素数さん:2005/09/06(火) 23:35:12
これが可能になったら数学者という仕事が無くなっちゃうの?

2 :132人目の素数さん:2005/09/06(火) 23:36:59
2

3 :132人目の素数さん:2005/09/07(水) 00:22:52
定理の自動証明が実用レベルに達してるなら他の大抵の仕事も実用レベルに達する。
その時にコンピュータには出来ないような新しい仕事を見つけられなければ
数学者だけでなく殆どの人間の仕事が無くなる。

4 :132人目の素数さん:2005/09/07(水) 00:34:23
で、
コンピュータによる定理の自動証明ってどうやるのさ?

5 :132人目の素数さん:2005/09/07(水) 10:58:40
趣旨とは違うが、「A=B」のような方向はもう少し発展すべきだと思う。

6 :132人目の素数さん:2005/09/07(水) 12:43:47
ゲーデルの考えが正しいとすると、機械には数学者と同じレベルの証明は、
永久に出来ないだろう。


7 :132人目の素数さん:2005/09/07(水) 12:53:17
>コンピュータには出来ないような新しい仕事
何が「美しい」か見極める事(新しくないけど)。
コンピュータの万能性の可能性を否定するにはそれだけで十分。

8 :132人目の素数さん:2005/09/07(水) 13:35:03
主観がない、ということか。

9 :132人目の素数さん:2005/09/07(水) 18:10:37
数学の概念を全て「記号」であらわすというのはライプニッツの目指したもの。
それを2進であらわせれば、コンピュータに数学をやらせる土台ができるかもな〜。

10 :132人目の素数さん:2005/09/07(水) 18:13:06
可能にはなると思うが、
「美しい証明」になるかどうかは別問題。

11 :132人目の素数さん:2005/09/07(水) 18:13:47
既にある証明のデータベース化は進んでないの?自動証明による証明の再現という意味なのだけど。


12 :132人目の素数さん:2005/09/07(水) 18:23:54
意味が概念として理解できなければ組合せの爆発により証明が終了しない。

13 :132人目の素数さん:2005/09/07(水) 20:16:39
数学にも哲学にも通じてる情報科学のあったまぃー人が解決してくれるんでしょ

14 :132人目の素数さん:2005/09/08(木) 00:23:02
以下マジレス
コンピュータによる定理の自動証明は今のところ「少し可能」という状態です。
事実、コンピュータで自動証明された定理も存在します。ただ、その証明はおせじにも美しい証明とはいえないが…
証明の内容は忘れたが、こんなことを前期の授業でやった。

15 :132人目の素数さん:2005/09/08(木) 00:48:41
四色問題か

16 :132人目の素数さん:2005/09/08(木) 01:31:06
>>15
たしか、二等辺三角形がどうたらってやつだった
四色問題は異論があるから微妙じゃない?

17 :132人目の素数さん:2005/09/08(木) 03:48:11
4色問題は、地図を幾つかのパートに分割して、
その全てのパートに対して定理が成り立つことを確認する所を
コンピュータにやらせたんだったっけ?
この場合、コンピュータは人間の作ったアルゴリズム通りに動作しているだけなので、
「自動」証明とは言い難いなぁ。
てか、自動証明って何?コンピュータが1から全部証明やってくれることでしょ?

18 :132人目の素数さん:2005/09/08(木) 07:33:41
四食問題は単に機械的にチェックできる部分をやらせただけなのでは。
微分方程式の数値解を計算機で出すか手計算でやるかの違いみたいな感じがする。

普通の自動証明というと、推論規則と命題を与えてその証明を作らせることかな?

19 :132人目の素数さん:2005/09/08(木) 08:47:53
定理の自動証明は公理から出発して定理が導けるまで動作を続けるか、
定理から証明に必要な公理を導き出す。

20 :132人目の素数さん:2005/09/08(木) 11:02:02
>>19
基本的には¬(公理⇒定理)から自動的に矛盾を導く。
証明が存在するなら、矛盾が導ける。
しかし、存在しない場合にはプロセスが終了しない可能性がある。

21 :132人目の素数さん:2005/09/08(木) 16:06:50
>>20

それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
例えば宇宙の原子の数なんて10^50程度のオーダーしかない。
ちょっと難しい定理の機械証明の探索論理ステップ数なんて
そんなオーダーの組合わせ数じゃ済まないんじゃないの?

22 :132人目の素数さん:2005/09/08(木) 16:45:14
「こういうときにはこの定理を用いる場合が多い」っつー傾向というのがありまして、
そういうメタ知識を用いると、かなりよくなります。

23 :132人目の素数さん:2005/09/08(木) 18:01:02
>>22

それは人間が発見した定理を利用するということ?
それはちょっとズルイというか、やっぱ人間が必要なんじゃないかと

24 :132人目の素数さん:2005/09/08(木) 18:03:40
>>23
なんじゃそりゃ、
もしや0から全てコンピュータに行わせようとしてるのか?
過去の資産を生かさずしてどうする。

25 :132人目の素数さん:2005/09/08(木) 18:08:21
いつまでも人間が面倒みなけりゃならないなら、こっちこそなんじゃそりゃ
と言いたくなるな

26 :132人目の素数さん:2005/09/08(木) 18:25:38
コンピュータは所詮道具なんだよ。
人間がやる定理証明に役立ってくれればいいの。
なんでもかんでもコンピュータにやらせる必要は無いの。

27 :132人目の素数さん:2005/09/08(木) 18:25:42
とりあえず定理のデータベースを作ってくれ。

28 :132人目の素数さん:2005/09/08(木) 18:31:02
>>5
A=B?

29 :132人目の素数さん:2005/09/08(木) 18:35:36
>>26
それで役立つんかい?
人間が証明出来ない定理をコンピュータが証明してくれるとか?

30 :132人目の素数さん:2005/09/08(木) 19:41:41
>>1
正しい定理を見つける仕事は残るだろう。

31 :132人目の素数さん:2005/09/08(木) 20:02:07
ときたまジョブをチェックする仕事は必須

32 :132人目の素数さん:2005/09/08(木) 20:08:24
人間に証明出来ない問題がコンピュータに証明出来るわけないわな。
コンピュータなんてただ計算が速いだけだし。難しい予想なんて解こうものなら既存の数学では無理な場合もあるし、
コンピュータがその道具を作っていくなんてまず不可能じゃね?

33 :132人目の素数さん:2005/09/08(木) 23:08:57
人間だろうがコンピュータだろうが鼠を取るのが良い猫だ。

34 :132人目の素数さん:2005/09/08(木) 23:14:10
コンピュータに快楽と苦痛を与えればなんでも出来る。

35 :132人目の素数さん:2005/09/08(木) 23:57:12
オダインに頼め。
エルオーネの能力に比べれば、証明なんて

36 :132人目の素数さん:2005/09/09(金) 01:31:54
>>34
強化学習も結局はx^nオーダーの計算量となるわけで

37 :132人目の素数さん:2005/09/09(金) 01:36:53
追試・データベース化、翻訳などに役立つであろう。


38 :132人目の素数さん:2005/09/09(金) 05:54:41
合流性とか停止性とかいう話があったよね>証明系

39 :132人目の素数さん:2005/09/09(金) 13:21:38
おまえらPrologは知ってるよな?


40 :132人目の素数さん:2005/09/09(金) 13:32:45
ああ、あの失敗したプロジェクトで使われた言語ね
第五世代コンピュータ開発計画とかいう税金のムダ使いで

41 :132人目の素数さん:2005/09/09(金) 13:55:07
プログラミング言語で一種のファッションだろ?

42 :132人目の素数さん:2005/09/09(金) 14:14:59
プログラミング言語は流行廃りが激しいから、数学者が勉強すべきものではないだろう。


43 :132人目の素数さん:2005/09/09(金) 14:37:44
自動証明⊆人工知能
と言える?
人間並みの人工知能ができれば、自動証明もできるはず。


44 :GiantLeaves ◆6fN.Sojv5w :2005/09/09(金) 17:03:36
証明作成のアルゴリズムとして、どんな方法がありうるのか?
検索の枝きりが難しいと思う。

45 :132人目の素数さん:2005/09/09(金) 17:40:48
あ、今アリゴリズム体操おわっちゃった。


46 :132人目の素数さん:2005/09/09(金) 19:04:07
こっち向いて二人で前ならえ
あっち向いて二人で前ならえ

47 :132人目の素数さん:2005/09/09(金) 22:58:51
>>28
> >>5
> A=B?
ググれ。

48 :132人目の素数さん:2005/09/09(金) 23:15:49
>>47
http://www.google.com/search?num=50&hl=ja&q=A%3DB&lr=lang_ja
http://www.google.com/search?num=50&hl=ja&q=A%3DB%E3%80%80%E8%87%AA%E5%8B%95%E8%A8%BC%E6%98%8E&lr=lang_ja
http://www.google.com/search?num=50&hl=ja&q=A%3DB%E3%80%80%E3%82%B3%E3%83%B3%E3%83%94%E3%83%A5%E3%83%BC%E3%82%BF&lr=lang_ja

ハァ?

49 :132人目の素数さん:2005/09/09(金) 23:30:32
ほらAIってあれだろっ!ドラクエ4に搭載の…

50 :132人目の素数さん:2005/09/10(土) 06:22:49
ボスに向かってザラキを唱えるやつか。

51 :132人目の素数さん:2005/09/10(土) 10:43:48
>>48
キミはgoogle の使い方を知らない。

52 :132人目の素数さん:2005/09/10(土) 11:07:15
この分野は日本では信州大が一番進んでいる
ようだよ。
お前らが大好きな数研の教科書書いてる方が
精力的に進めている

53 :132人目の素数さん:2005/09/10(土) 11:46:30
>>52
mizarは"theorem prover"ではなく"proof checker"ですよ。
checkerでさえ現状ではライブラリ不足で実際に数学では使えないでしょう。

54 :48:2005/09/10(土) 13:48:10
>>51
ではどのようにすればA=BでGoogleで検索できるか教えていただけますか?

(´-`).。oO(二重引用符でくくれとかそういうオチかな?)

55 :名無しさん@そうだ選挙に行こう:2005/09/10(土) 23:49:29
挑発したら教えてもらえなくなるよ

56 :48:2005/09/10(土) 23:53:25
はいはいヽ(´ー`)ノ

57 :名無しさん@そうだ選挙に行こう:2005/09/11(日) 19:18:21
>>53
ライブラリ不足かどうかは知らんが、そもそも現実の数学研究で使えるような
表現力を持つ言語を処理させるのはきついんじゃなかろうかと思う。

>>54
俺も気になる。
「A=B」みたいなのをキーワードにしてGoogleで有意義な情報を引き出せるのか?
まあ元々の発言(>>5)の言わんとするところはわからなくもないが。


58 :名無しさん@そうだ選挙に行こう:2005/09/11(日) 22:54:00
コンピュータにPeano算術での自動証明プロセスを与えて、
しらみつぶしで¬(0=0)の証明を探索させたら、
もしかしたら有限時間内に「証明あり」って出力が返る可能性がある?
もしそうなったらどうなるの?

59 :名無しさん@そうだ選挙に行こう:2005/09/11(日) 23:03:14
>>58
PA が矛盾してるならあるかもね

60 :名無しさん@そうだ選挙に行こう:2005/09/11(日) 23:31:38
>>59
こえー。そしたら帰納法使った証明が全ておじゃんだしZFとかも壊滅だし。
>>58の自動証明を延々走らせてる不信心な暇人っていないのかな。

61 :132人目の素数さん:2005/09/12(月) 08:30:11
A=B 等式証明とコンピュータ, 1997 トッパン
トッパンが2000年に出版事業から撤退したため、あまり知られてない。
幸い原本がpdfで公開されている。クヌースによる序言だけでも読むことを勧める。

http://www.cis.upenn.edu/~wilf/AeqB.html

62 :132人目の素数さん:2005/09/12(月) 17:01:24
>>21
>それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
人間もバカチョンでしらみつぶしに探してる。意識してないだけ。

人間が証明を見つけるまでの間にもそれこそ長い年月を必要としている。
今のコンピュータよりも人間のほうが優れているかもしれんが
それこそ非常に長い時間をかけた進化の結果である。

63 :132人目の素数さん:2005/09/12(月) 17:05:14
>人間もバカチョンでしらみつぶしに探してる。意識してないだけ。

嘘だろ

64 :132人目の素数さん:2005/09/12(月) 17:12:09
>>63
残念だが本当だ。
ところで、誰かTarskiの量化記号消去について簡単に説明してくれ。

65 :132人目の素数さん:2005/09/12(月) 17:21:28
>>64

話をそらすなよ。しらみつぶしなわけないだろ
しらみつぶしだったら時間がかかりすぎ。

66 :132人目の素数さん:2005/09/12(月) 17:34:00
>>65
いや、そのくらい時間がかかるのが当然なんだ。
それより、質問したことについて知らないなら黙っててくれ。
無知な奴と遊んでる暇はないんだ。

67 :132人目の素数さん:2005/09/12(月) 17:41:41
>>66

時間がかかりすぎというのは100年とか200年のオーダー
じゃないんだよ。現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。

68 :132人目の素数さん:2005/09/12(月) 17:43:51
>>67
>現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。

君以前の人がそうしている。
君がその知識を利用しているときに
そのことを意識できないだけ。

69 :132人目の素数さん:2005/09/12(月) 17:58:40
>>68

過去の知識といっても膨大。
その膨大な知識をしらみつぶしに調べてるわけじゃない。

70 :132人目の素数さん:2005/09/12(月) 18:02:23
彼の「しらみつぶし」って単語の定義が俺様独自定義なんだろ

71 :132人目の素数さん:2005/09/12(月) 18:26:37
昔の人がすでにしらみつぶしに調べてきたから今の人はそうする必要がないという理屈だな


72 :132人目の素数さん:2005/09/12(月) 18:51:19
例えば将棋で次の一手をしらみつぶしで探せるはずがない。
それと同じで証明もこうすればよさそうだ、とある程度見切りをつけて行っているはず。
直観力+構成力+知識・経験が物を言う。

73 :132人目の素数さん:2005/09/12(月) 18:54:43
>>71

その昔のひとが得た結果の組み合わせの数だって膨大。
それを、しらみつぶしに調べてるわけない。

74 :71:2005/09/12(月) 19:28:09
>>72
我々がそういう力を持ってるのは昔の人がしらみつぶしにやって得た知識を
受け継いでるからだと考えることもまったく不可能なわけではないんじゃない?

>>73
まあそうかもしれないとは思うけど、自信を持って言い切れる理由があるの?

一応言っとくと、>>62 を積極的に支持するわけじゃないよ。
けど、間違いだという根拠も持ってないし、
部分的には正しいように思えるからあえてこういうレスをしてみた。

75 :132人目の素数さん:2005/09/12(月) 20:19:54
コンピュータで証明するときに、あらかじめ「知識」のデータベースを入れて
それ使って証明しても「しらみつぶしで証明しました」って言うわけか?

76 :132人目の素数さん:2005/09/12(月) 20:31:51
しらみつぶしって言うのは、たとえて言うなら、10回戦のトーナメント方式の1回戦から全ての対戦を行うことに例えれば。
知識があるっていうのは、経験則でこの対戦は無いってシードの部分がいくつかあって考慮する必要のない部分があるってことでしょ。

77 :132人目の素数さん:2005/09/12(月) 20:39:10
今使ってるパソコンでも、π=3.14・・・とかはいちいち計算しないで使われてるんだろ?

78 :132人目の素数さん:2005/09/12(月) 20:39:15
意味を理解しているならばしらみつぶしに探索しなくてよい。

79 :132人目の素数さん:2005/09/12(月) 21:35:02
おまえら、せめてヒューリスティックスって言葉使えよ・・・

80 :132人目の素数さん:2005/09/12(月) 21:37:47
うむ、そういえばそんな言葉があったな。
最近使ってなかったせいか忘れていた。

81 :132人目の素数さん:2005/09/12(月) 21:39:37
>>77
ヒューリスティックスなしらみつぶしで、「知識」のデータベースを
元に計算してまつ

82 :132人目の素数さん:2005/09/12(月) 21:43:39
>>81
ワロスw

83 :132人目の素数さん:2005/09/13(火) 13:45:06
とにかくこのスレは不毛。人間の知能の仕組みなんて誰もなーんも
わかっちゃいない。それをコンピュータでシミュレート出来るわけがない。
映画とかSFでは人間なみのロボットが出てくるけど、そんなのまさに
夢物語。人口知能の研究者ってのは鉄腕アトムの読みすぎ。
定理の証明というのは人間の知的能力の一部だけど、まるで解明

84 :132人目の素数さん:2005/09/13(火) 13:49:55
書き込んでる最中に暗殺された>>83のご冥福をお祈り致します。

85 :132人目の素数さん:2005/09/13(火) 16:01:37
>>72
>証明もこうすればよさそうだ、ある程度見切りをつけて行っているはず

それはしらみつぶしとは矛盾しない。
単に深さ優先探索ではないというだけ。

86 :132人目の素数さん:2005/09/13(火) 16:04:24
>>83-84
ワロスw

87 :132人目の素数さん:2005/09/13(火) 16:04:25
>人間の知能の仕組みなんて誰もなーんもわかっちゃいない。
>それをコンピュータでシミュレート出来るわけがない。

・・・というより、シミュレートしていたとしても
それに気づくことができないというべきか。

ところで数学の定理の証明がすばらしいものだ
という考えは数学をやっている人間の個人的感情
に過ぎない。

88 :132人目の素数さん:2005/09/13(火) 16:30:30
>>87

定理の証明が出来るということは不思議な能力だという考えは?

89 :132人目の素数さん:2005/09/13(火) 16:38:48
>>88
不思議とは無理解のことである。

90 :132人目の素数さん:2005/09/13(火) 17:06:41
この場合は無理解というより不可解

91 :132人目の素数さん:2005/09/13(火) 17:51:05
地球の原子すべてをシミュレーション出来るコンピュータが出来たら生物はもちろん文明さえもシミュレーション
出来るのではないか。

92 :132人目の素数さん:2005/09/13(火) 18:10:57
>>91

データをどうやって入れるんだよ

93 :132人目の素数さん:2005/09/13(火) 18:15:55
>>91
そのコンピュータは自分自身をシミュレートするのか?

94 :132人目の素数さん:2005/09/13(火) 18:53:47
哲学的な問いでなかなか面白いでつね。

95 :132人目の素数さん:2005/09/14(水) 00:02:45
>>94 
チューリングマシン
とか
停止問題
でぐぐってみ。否定的な結論が出るから。

96 :132人目の素数さん:2005/09/14(水) 06:20:52
証明すべき命題をどう符号化するか、という問題がまずある。
もし、すべての数学定理が計算機で証明できるならば、
たったひとつのアルゴリズムから、次々に定理を自動生成できるんじゃなかろうか?
そんなアルゴリズムが果たして存在するのか?

97 :132人目の素数さん:2005/09/14(水) 07:14:49
>>96
ZFC を計算機で書けばいいわけだから原理的には余裕でできる
けどなんか工夫しないと時間かかりすぎて意味のある定理はほとんど出ないと思う

98 :132人目の素数さん:2005/09/14(水) 07:39:17
>>96
くそ定理は山程合成出来る。

99 :132人目の素数さん:2005/09/14(水) 09:30:09
人間機械論を否定したゲーデルの論文があると聞いた。
彼の不完全性定理を基にしている。
人工知能を研究している人なら知ってるよね?

100 :132人目の素数さん:2005/09/14(水) 10:21:30
>>93
コンピュータをシミュレーションするコンピュータはターゲットのコンピュータより
メモリは大きくスピードも速くなければならない。

101 :132人目の素数さん:2005/09/14(水) 10:31:37
そんなことより地球シミュレータのデータのほうが問題だろ。
全ての原子のデータなんてわかるわけがない。
可能性があるとしたらBig Bangのシミュレータ。
仮に出来たとしても地球が出来るまで相当時間がかかるw

102 :132人目の素数さん:2005/09/14(水) 18:28:09
>>100
確かにメモリは大きい必要があるが、
スピードに関しては遅くても構わない。
ただし、もちろん実物より遅くなってしまう。
用途によっては実物より遅くても、結果の再現が得られれば良い場合もある。
例えば新しいCPUの回路設計など。

103 :132人目の素数さん:2005/09/14(水) 18:29:11
>>98
文字通りトリビアの泉になるわけだな……。

104 :132人目の素数さん:2005/09/14(水) 18:46:14
山田君、座布団1枚もっていki(略

105 :132人目の素数さん:2005/09/14(水) 19:38:13
停止性問題しかり、ディオファントス方程式しかり、計算機で証明できない問題はたくさんあるわけで。
「定理」は有限文字列で表現できるから
「この世のすべての定理」を列挙することは一応できるけど
それらすべての真偽を判定することはできないと言うことか。

106 :132人目の素数さん:2005/09/14(水) 22:21:08
>>105
証明できないものを定理とは呼ばないんじゃ?
それでも定理全てを列挙することは出来るが。

107 :132人目の素数さん:2005/09/14(水) 22:29:02
最近のコンピュータ将棋って結構強いよね。
ルールや対局データを与え、アマチュアには勝てるようにプログラムされている。
自動証明も同じようにできそうだけど、案外自動証明を研究されている方がプログラミングが不得意なのかもしれないよ。
私の従兄弟は数学のセンスは凄いのだけど、プログラムはてんで組めないんだよね。



108 :132人目の素数さん:2005/09/14(水) 22:34:56
>>106
ゴメンナサイ。「定理」ではなく「命題」と言うべきでした。

109 :132人目の素数さん:2005/09/14(水) 22:41:57
一応確認すると、定理全体の集合は recursively enumerable ですよね?

110 :132人目の素数さん:2005/09/14(水) 22:49:06
>>107
自動証明は将棋みたいに特化したものじゃないから同じようには無理だと思うよ。
あと数学のセンスとプログラム組む能力は関係ないと思う。
そもそもプログラムと一括りにしているが、使う言語がCかLispかでも
だいぶ違うんじゃないか?
ちなみに俺の友達には、高校数学のアルゴリズムの項目は
BASICじゃなくて関数型言語を使うべきとかいってるヤツがいるぞ。

>>108
どんまい


111 :132人目の素数さん:2005/09/14(水) 22:50:40
>>109
そうだよ

112 :109:2005/09/14(水) 22:53:18
そうですよね。
>>105を見るとそうでないように読めたので気になったので。

113 :109:2005/09/14(水) 22:57:33
あれ、そうでないように読めたのが勘違いか。
有限時間内に真偽を判定することはできませんね。
どうもすいません

114 :132人目の素数さん:2005/09/14(水) 22:58:33
>>110
高校数学の本閲覧したけど…1社だけ、JavaScriptだなw
確かに、関数型を通り越して、オブジェクト指向言語だわ。
で、こんなの勉強していちいち

 <html><head>
   <script language="JavaScript">
   <!--
           スクリプト本体
   //-->
   </script>
   <head>

 なんて、訳もわからず入力しているの想像すると…コピペするにして
も、何か非常に可哀想になってくるんですけど。

そりゃ、「極一部」のソフトで飯食おうとするヤツは別だろうけどさあ。大体、
そんなヤツは学校じゃなく自力で覚える!


115 :132人目の素数さん:2005/09/14(水) 22:59:36
情報科学の人も、プログラミングできる人の方が少数派なんでしょ?

116 :132人目の素数さん:2005/09/14(水) 23:03:04
>>112
r.e.だけだと偽かどうかを判定する手続きが止まらない可能性があるから
そういう意味では真偽を判定出来ないとも言える。
decidable(=recursive)ではないってことだ。

117 :132人目の素数さん:2005/09/14(水) 23:08:18
>>114
>高校数学の本閲覧したけど…1社だけ、JavaScriptだなw
マジ?!!
これで勉強させられるヤツら悲惨だな…。
本質的でない部分が多く含まれる上に、どうせ教える側も良くわかってないんだろうし。


118 :132人目の素数さん:2005/09/14(水) 23:20:28
>>117
まともな、高校数学教師なら、その教科書のその部分は「飛ばすべき」だ。
後で、校長や教頭から文句がくるやも知れないが、その方が「良心的」だと思う。

119 :132人目の素数さん:2005/09/15(木) 08:52:32
>>110
C言語でLispコンパイラを書けばいいじゃないか。

120 :132人目の素数さん:2005/09/15(木) 08:55:41
>>119
コンパイラを書くと何がいいの?

121 :132人目の素数さん:2005/09/15(木) 09:08:46
>>105
>「この世のすべての定理」を列挙することは一応できるけど

「この世のすべての定理」って、意味がよくわからない。
現在人類に知られている定理のすべてっていう意味?
因みに、当然だけど、可算無限集合の要素を有限時間内にすべて列挙する
ことは出来ない。

122 :132人目の素数さん:2005/09/15(木) 09:34:54
>>99
>人間機械論を否定したゲーデルの論文があると聞いた。

岩波の文庫本だったか啓蒙的な本を読んだだけなので詳しいことは
わからないけど、ゲーデルの趣旨は多分、以下のようなことだろうと
想像する(この想像が間違っていることも大いに有り得る)。

不完全性定理は機械には証明できない。よってそれを証明した
人間(ゲーデル)は機械では有り得ない。

123 :132人目の素数さん:2005/09/15(木) 10:52:13
人間機械論は人間と機械論が正しいと聞いたが、

124 :132人目の素数さん:2005/09/15(木) 10:58:28
それはどうでもよくて、>>122のゲーデルの趣旨は、人間の頭脳は
チューリングマシンのような機械ではないということ。

125 :122:2005/09/15(木) 11:50:58
>>122
>不完全性定理は機械には証明できない

自分で言い出してなんだけど、これ本当かな。
原理的には機械にも可能なような気もするな。
もしそうならゴメン

126 :132人目の素数さん:2005/09/15(木) 11:51:30
確かに人間の脳はチューリングマシンと違うよね。もしかしたらチューリングマシンにノイズの項を追加すると人間の脳と等価になったりして。ゲーデルはきっとノイズが大嫌いだよね(独断と偏見)。

ちょっと唐突だけど、ピタゴラス数( a^2 + b^2 = c^2 ) の基本解についてはかなり昔から知られていたよね。
基本解を導く手順のなかに「cは奇数である」とか「aかbのどちらか一方だけが偶数」なんていうのが現れる。そして最後にいくつでも簡単にピタゴラス数を計算できる方法を導いている。「昔なのにすごいなぁ」などと感心したもんですよハイ。

ピタゴラス数の基本解の導き方は今の中学生でも簡単にできる問題なので、自動証明のプログラムの例題としても比較的簡単そうだし、もしかしたら既に誰かがやっていると思うんだけどなあ。でもニュースなどでこれに近いことすら聞いたことがないのですよハイ。

127 :132人目の素数さん:2005/09/15(木) 12:32:01
あまり意識してないけど、俺が証明を考えるときは、たぶん、
その定理に使えそうな命題をいくつか組み合わせて推論し、
それが成功しないときは別の組み合わせを試す。つまり試行錯誤。
組み合わせというより、いろいろな方法と言ったほうがいいかもしれない。
定理によっては証明のパターンというものがある。
この種の定理にはこの方法を使うというような。
だから、問題を解く経験を含めた広い意味の知識というのは大きな要素
であるのは間違いないと思う。

128 :132人目の素数さん:2005/09/15(木) 13:23:13
ある種のノイズが関係していることは十分考えられる。
量子力学的ゆらぎとか。
そのノイズによりひらめきが誘発されるとか。

129 :132人目の素数さん:2005/09/16(金) 16:56:49
>>不完全性定理は機械には証明できない
>自分で言い出してなんだけど、これ本当かな。
もちろん初歩的な誤り。
不完全性定理は形式的証明が可能。
証明できないのはゲーデル命題。
もっとも、人間にも証明できないわけだが。

130 :132人目の素数さん:2005/09/16(金) 22:46:54
例えば、三角形の定義を入力すると三角形に関するありとあらゆる定理(クソなのも含めて)を生み出す
ってことは出来るのかな?

131 :132人目の素数さん:2005/09/16(金) 23:33:14
公理や推論規則も入力すればできる

132 :132人目の素数さん:2005/09/18(日) 04:33:41
初等幾何の証明はどうするんだろう。
図は別に使わないだろうけど、補助線の考え方自体は要るよね。
あれは激しくセンスが必要な気がするんだが…。

133 :132人目の素数さん:2005/09/18(日) 05:48:57
・・・え?

134 :132人目の素数さん:2005/09/18(日) 11:17:39
ところで、数学の定理って有限?

135 :132人目の素数さん:2005/09/18(日) 11:57:54
夢幻

136 :132人目の素数さん:2005/09/19(月) 00:33:41
>>132
適当に総当たりで補助線引いてみて、過去の定理を当てはめることができるか、
総掛かりで検索する…とか。

137 :132人目の素数さん:2005/09/19(月) 11:58:12
>>134
家産

138 :132人目の素数さん:2005/09/19(月) 15:04:55
>>132
証明の方法まで指定するのか?
コンピューターで計算するんなら、座標やベクトルを使うことになるんじゃないのかな。

139 :132人目の素数さん:2005/09/21(水) 14:20:02
* 任意の命題を証明するアルゴリズムは無い。

この前提となっているのは、「アルゴリズム」として、
有限長のものをどんな命題にも先立って与えるとしたら、
ということです。
命題を与えられてからそれを観た後であれこれとアルゴリズムを
生成していって、一般には有限個とは限らずに無限のアルゴリズム
列を作っていきながら判定を試みるというやり方であれば、
どうなるのかについては証明法の範囲外であると思います。
(この場合、「アルゴリズム」の列全体は可算ではないのです)

140 :132人目の素数さん:2005/09/21(水) 15:46:10
問題:
数学的帰納法で証明できる自然数の定理は、
すべてコンピュータで自動証明できるか?

141 :132人目の素数さん:2005/09/21(水) 22:05:49
No かな?

ペアノの公理系の帰納法は、自然数の集合あるいは自然数の命題に関する公理。
ペアノ算術の帰納法は、初等的命題に関する公理スキーマであり適用範囲が制限される。

このため人間が数学的帰納法により証明できる自然数の定理であっても、
その証明を一階述語論理+ペアノ算術で形式化できない可能性がある。

142 :132人目の素数さん:2005/09/22(木) 08:03:10
Yesだな!

ペアノの公理系は形式化されたもの。
証明があるなら当然コンピュータで自動証明できる。

しかし証明がない場合には延々と止まらない。
したがって、有限時間で全ての定理を
証明し切ることはできない。

143 :132人目の素数さん:2005/09/22(木) 15:14:37
人間だって有限時間で全ての定理を証明する事はできないジャン

144 :132人目の素数さん:2005/09/22(木) 18:10:03
>>143
人間ならできる!といった覚えは一度も無いが

145 :132人目の素数さん:2005/09/22(木) 21:22:11
帰納法使えばいいじゃない

146 :132人目の素数さん:2005/09/23(金) 05:21:34
>>139
それは命題を入力として証明手続きを列挙する手続きの存在を仮定してるから
結局同じことなんだが。
あと真でない命題を入力した時に有限時間内に終わらない可能性がある。
最終行の可算は有限の間違い?

147 :132人目の素数さん:2005/09/23(金) 15:41:29
いや、ちょっと架空の話で例示してみよう。
(本当はこういうことはないのだが、N文字で書かれた任意の命題を
証明することのできる・あるいは否定できる手続きのプログラムで
10^10^N文字以内で書けるものが常に存在する、
というようなことがあったと仮にしてみよう。もちろん嘘だが)
もしもそうであれば、
そのとき、ある任意の命題(その長さをN文字としよう)
が与えられたとして、それから始めて、10^10^N文字以内の
プログラムをすべて列挙して調べれば原理的には答えがわかる
ということになる。

 ところが、全く任意の命題が与えられるとするならこの方法は使えない。
なぜならNが事前には抑えられていないので、予め有限長のプログラムを
用意しておくなどということが出来ないのだ。

つまり、もしも、このような状況であれば、
やってきた入力を観た後からだと可能である。ところが
どんな入力が来ても処理できるように事前に準備することは
出来ない、のである。

148 :132人目の素数さん:2005/09/29(木) 16:19:50
295 :132人目の素数さん :2005/09/29(木) 11:58:46
夫馬です。

黒木先生。この基礎論・計算科学屋を叩いて下さい。

「完全証明」という専門用語を使い、「今まで数学
的に完全な証明がなかった!」というように素人に
思い込ませる。コケオドシをやっています。ポモ的
です。やっつけて下さいな。

>フランスの数学者カミーユ・ジョルダンが1887年に概念を確立し、その後多くの
>数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
>工学部の中村八束(やつか)教授(62)が27日、ポーランドの数学者ら16人との
>約14年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
>などを確認するコンピューターシステムのチェックを経て、約20万行にわたる証明が
>完成。中村教授らは「完全証明したのは世界初」としている。
http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html

149 :132人目の素数さん:2005/09/29(木) 16:23:20
土建屋、宇沢、長谷川、黒木の数理物理、可積分系、表現論自体が
コケオドシだから、黒木にこいつらを叩く資格はないよw

150 :132人目の素数さん:2005/09/29(木) 16:25:11
301 :132人目の素数さん :2005/09/29(木) 15:12:47
>>295
この中村って香具師、あほ鴨の仲間じゃねーか?


302 :132人目の素数さん :2005/09/29(木) 15:16:20
>>301
ポモ的なのに叩かないのは、そういう理由だったんだね!

土建屋=宇沢=長谷川=黒木 ← 隠れポモ野郎
禿藁=U健爾 ← 隠れポモ野郎
あほ鴨=中村 ← 隠れポモ野郎


303 :132人目の素数さん :2005/09/29(木) 15:26:53
>>302 >>295
こいつらって、結局
ポモと同じでしょ。

>そして、別の場所で、極端なことを言っているのではないかと非難された場合には、
>3 (a) に近い穏健だが当たり前の主張を述べて批判をかわします。
http://www.math.tohoku.ac.jp/~kuroki/FN/relativism.html

151 :132人目の素数さん:2005/11/10(木) 18:44:30
552

152 :132人目の素数さん:2005/11/10(木) 20:55:41
記号論理学が嫌われるのは、命題という、数のようにモノと思いやすくない
ものまでAとかBとかいう記号で扱うことに対して、無意識の不安、抵抗
があるからであろう。
これを払拭させるには、まず。「命題はモノではない」ということを
明確に意識させたうえで、「それでも命題は或る意味でモノ扱い出来る」
ということを相当徹底的に理解させることが有効であろう。

尤も、この第2段階で徹底的に抵抗するような人物には、この教育法も
無力であろうが、記号論理学嫌いのほとんどは、第1段階によって、自分
の記号論理学嫌いの原因を明確に意識出来れば、次の第2段階も突破する
であろう。
そうなれば、定理の自動証明の基本構想の概念に到達し易くなるであろう。
このスレッドの話はそのあで始めるのが良いだろう。

153 :132人目の素数さん:2005/11/10(木) 20:58:37
そのあで ー> そのあとで

154 :132人目の素数さん:2005/11/10(木) 21:18:05
>>152
そういった内容は認知心理学でいうメタ知識に相当するから、
いわば「公理の公理」としておさえておくことが好ましい。


155 :132人目の素数さん:2005/11/10(木) 22:11:50
記号論理学の見た目の記号がつまらん。

156 :132人目の素数さん:2005/11/11(金) 17:49:54
記号論理学って嫌われてるのか?
どういう人に?

157 :132人目の素数さん:2005/11/12(土) 07:28:14
大統一数学理論ってないですかね。

158 :132人目の素数さん:2005/11/12(土) 17:40:12
人間の脳みそで出来るんだからコンピューターにだって出来るだろ

159 :132人目の素数さん:2005/11/12(土) 17:44:11
今のコンピュータじゃかなり難しいだろ

160 :132人目の素数さん:2005/11/13(日) 15:22:48
出来たとき有益で人々から感謝されるならば作る価値がある。

161 :132人目の素数さん:2005/11/16(水) 20:43:05
不完全性定理の証明とか見るとわかるが
コンピュータに足りないのは定義を増やすという操作なわけだよ

162 :132人目の素数さん:2005/11/18(金) 07:41:45
age

163 :132人目の素数さん:2005/11/18(金) 07:44:37
定義を増やすぐらい出来ているが・・・

164 :132人目の素数さん:2005/11/18(金) 07:50:48
融通が効くかどうかが重要なのね

165 :132人目の素数さん:2005/12/12(月) 18:46:27
924

166 :132人目の素数さん:2005/12/12(月) 19:03:53
コンピュータが出来てから10年くらいたったころだから今から
50年位前に計算機科学の有名な学者が10年以内に定理の
自動証明が出来るだろうと予言した。だから専門家といってもなーんも
分かってないんだよ。現在だって同じ。

167 :132人目の素数さん:2005/12/12(月) 22:52:38
しらみつぶしに証明のゲーデル数が小さい方から
定理を全て証明していくつもり、、だったんだろうかな
何の見積もりを間違えたんだろう?
実際の定理の複雑さか計算機のスピードか

168 :132人目の素数さん:2005/12/13(火) 09:31:57
ノイマン式コンピュータじゃ無理だろ。
ま俺は専門家じゃないからあてにならないがw
今のコンピュータというのは原理的には50年前と同じ、
つまりノイマン式。これをいくらいじっても無理だろう。

169 :132人目の素数さん:2005/12/13(火) 14:34:14
四色問題はチェック作業を機械化しただけであり、自動証明とは言えない。
しかし証明に携わった人間によれば、時折コンピュータが
人間以上の「知性」を垣間見せることがあるという…。

170 :132人目の素数さん:2005/12/13(火) 14:37:46
>>169

時折垣間見せるじゃ駄目だろ。俺みたいにチューリングテストに
パスしないと。

171 :132人目の素数さん:2005/12/13(火) 17:18:15
Kingって結構チューリングテストに合格しなかったりしてw

172 :132人目の素数さん:2005/12/13(火) 17:18:46
ってか自動証明の話してるときにチューリングテストの話せんでもいいだろ

173 :GiantLeaves ◆6fN.Sojv5w :2005/12/13(火) 22:18:30
talk:>>171 何やってんだよ?

174 :132人目の素数さん:2005/12/13(火) 22:22:56
いやいかにも
talk:>>とか自動生成っぽいなとか思ってw

175 :132人目の素数さん:2005/12/14(水) 09:08:39
>>172

冗談通じないのね。

176 :132人目の素数さん:2005/12/20(火) 06:34:18
定理の自動証明なんて散々研究されてる分野なんだが
なんで出来ないとか主張してる奴がいるんだ?

せめて「定理 自動証明」でググれ

177 :132人目の素数さん:2005/12/21(水) 14:46:23
age

178 :132人目の素数さん:2005/12/21(水) 15:21:45
>なんで出来ないとか主張してる奴がいるんだ?

(証明が自明な定理は除いて)出来てないから。

179 :132人目の素数さん:2005/12/21(水) 17:38:44
研究されてるのと、実際に実現してるのは別だよね
AIも然り

180 :132人目の素数さん:2005/12/21(水) 22:49:10
コンピュータのスピードさえ上がればえらいことになるだろ?
暗号だけじゃなくて定理証明も。
量子コンピュータとかが実用化したら、、、?

181 :132人目の素数さん:2005/12/22(木) 01:48:46
そうかなあ、、結構オーダーが違うと思うけど、、
第一コンピューターがそんなに早かったら
気象学も分子生物学も量子化学も今より進歩してるはずだよw

182 :132人目の素数さん:2005/12/22(木) 10:42:15
181の2行目以降は無意味。


183 :132人目の素数さん:2005/12/22(木) 11:28:53
>>1
コンピューターが何かわかっていない。考える機械だとでも
思っているのか。人間が作ったソフトウェアを実行するのみ。
計算とかは得意だから全部計算してみるとか、数え上げるなんて
ことはできるだろう。いずれにせよ有限個のみ。

184 :132人目の素数さん:2005/12/22(木) 21:44:13
人間の脳だって化学反応の連鎖で動いているだけだけどな

185 :132人目の素数さん:2005/12/22(木) 23:19:51
人間が証明出来る数学の命題式も有限個にすぎない。
今までに書かれた全ての数学の論文、書籍を論理過程の
省略を無くして書き直したとしても、使われる文字の
総数は有限個に過ぎない。「任意の実数に対して成り立つ」
とかいう有限個の文字の思考で無限個のことが分ったつもり
になっているに過ぎない。
コンピュータによる定理の自動証明は可能と言ってよい。
ただコンンピュータの速度が飛躍的に増大すればいい。
証明された定理のうち、人間にとって意義あると思われる
ものを選び出すのは人間の仕事となるだろう。
コンピュータが脳と「同様に」働かなくても良い。脳が証明する
のと「同じ」定理を噴出しつづければばいい。
「ピッチングマシンが人間の投手と「同様に」働かなくてもいい。
 人間が投げるのと「同じ」タマを発射すればいい。」
 というのと同様。

186 :132人目の素数さん:2005/12/23(金) 06:41:52
>証明された定理のうち、人間にとって意義あると思われる
>ものを選び出すのは人間の仕事となるだろう。
そんな100億(くらい少なけりゃまだ良いがw)の芥の中から
1個の宝石を選び出す仕事が成立すると思うのかねw

数学者の人生の99%は無意味な定理の吟味に費やされるぞw

187 :132人目の素数さん:2005/12/23(金) 08:05:42
>人間が証明出来る数学の命題式も有限個にすぎない。
これはいいとしても
>「任意の実数に対して成り立つ」
>とかいう有限個の文字の思考で無限個のことが分ったつもり
>になっているに過ぎない。
実際どんな実数ほうりこんでも「任意の実数に対して成り立つ」
定理はなりたつでそ。しかも証明までされてるんじゃ文句言えない
でしょ。あなたは数学の証明で使われる論法はでたらめだと言いたい
のですか。コンピューターで片っ端から数を代入しても成り立つ
はずです。でもコンピューターでは有限の数しか扱えないので
無理数は扱えない。この辺がコンピューターの限界。

188 :132人目の素数さん:2005/12/23(金) 08:13:55
>人間の脳だって化学反応の連鎖で動いているだけだけどな
これも科学者の作り出した単純な世界観にすぎない。
こんなもので普遍的に正しいものが捕らえられるだろうか。
進化論を全員まじめに信じるのは日本人だけで、科学先進国
欧米ではそんなこと全然ないということは知っておくべき。

189 :132人目の素数さん:2005/12/23(金) 08:47:05
>>187
でたらめじゃなくて、有限個の文字で表現できる思考で
無限のことを考えて、その程度の思考でとらえられる
無限のからむ真理ぐらいまでしか分っていないと言って
るの。
人間が無理数を考える思考も、ある様式に則って表現
すれば、有限個の文字で表されるだろ。それをコンピュ
ータで扱うことも出来ることになるという筋。
これぞ記号論理の原理のひとつでしょ。これを拒絶する数
学屋が多い(?)のは不思議。

190 :132人目の素数さん:2005/12/23(金) 08:47:28
>でもコンピューターでは有限の数しか扱えないので無理数は扱えない。
代数的数なら頑張れば扱える気がするけどね
扱い方工夫すれば

>>188
>進化論を全員まじめに信じるのは日本人だけで、科学先進国
>欧米ではそんなこと全然ないということは知っておくべき。
欧米で進化論を真っ向から否定するのは、
プロテスタントの狂信者くらいしか居ない訳ですが、、

進化論は間違っている、なぜなら聖書に書いてないから、とか物凄く
「科学的」なことを言う人たちね

とりあえずおまいさんは「利己的な遺伝子」嫁
話はそれからだ

191 :132人目の素数さん:2005/12/23(金) 08:55:10
コンピューターで扱っているのは有限の2進数だから
近似値としての無理数以外扱えない。無理数の近似値
は有限の数、すなわち有理数のなかで有限のものだけ
しか正確には扱えない。これで様子を調べるとか近似値
を求めることはできる。科学実験ではそれで十分かも
しれないが数学はそういう立場ではないでそ。

192 :132人目の素数さん:2005/12/23(金) 09:02:15
>欧米で進化論を真っ向から否定するのは、
>プロテスタントの狂信者くらいしか居ない訳ですが
こういう風にカルトしか単純な科学的世界観を否定しない
などと思っているのは日本以外の文化を知らないから。
ニュートン力学の神も仏もない世界観に対する議論は
さんざんされて、結局一部の狂信的な科学信奉者以外
受け入れてはいない。ニュートンに代わってアインシュタイン
がもてはやされる理由はこのあたりにもある模様。

193 :132人目の素数さん:2005/12/23(金) 09:07:34
人間にとって有益な定理は複数の命題から単純な命題を導き出すからコンピューターの糞定理からそんな形式を抜き出せば
比較的簡単に見付かる。

194 :132人目の素数さん:2005/12/23(金) 09:09:49
>>189
修正。「記号論理の原理」じゃなくて「記号論理の効用」
原理は別にある。
>>191
そう言う次元の話じゃないの。「記号論理の原理」について
10冊ぐらいの本で10ヶ月ぐらいかけて考えてくれ。留年
覚悟で。尤も、本人に時期が来てないなら、それでも分らん
だろうが。
分らなくてもいい。走りの原理が分らなくても走れれば
素晴らしいから。

195 :132人目の素数さん:2005/12/23(金) 09:11:12
無理数の話
>ttp://www.gakushuin.ac.jp/~881791/d/0508.html#15

>>192
>ニュートン力学の神も仏もない世界観に対する議論は
>さんざんされて、結局一部の狂信的な科学信奉者以外
>受け入れてはいない。
世界観は兎も角としてニュートン力学自体は受け入れているんでしょ
アインシュタインは別にニュートン力学が根本的に間違っていることを示したんじゃなくて
エネルギーが高い場合に出来る誤差を修正した、と考えるべき

大体科学と言ったって、究極的には、そう考えるのが最も尤もらしい、という以外の
根拠なんて無いんですよ
実験環境を整えてある実験をしたところ99回とも同じ、面白い結果が出た
で、100回目に同じことをしたら、やはり同じ結果が出るだろう、と推測するのが科学
いや、そうとは限らない、と考えるのが哲学

196 :132人目の素数さん:2005/12/23(金) 09:12:50
数学は?


197 :132人目の素数さん:2005/12/23(金) 09:15:08


198 :132人目の素数さん:2005/12/23(金) 09:20:28
>実験環境を整えてある実験をしたところ99回とも同じ、面白い結果が出た
同じ実験をして違う結果がでると実験屋さんたちは認めないんでしょ。
数学の反例みたいなもんで。現実はわからんのをいいことに捏造なんか
もあるかもしらんが。


199 :132人目の素数さん:2005/12/23(金) 09:38:51
2^(1/2)

うわっ
コンピュータ上で無理数を表しちゃったよ。どうしよう


200 :132人目の素数さん:2005/12/23(金) 09:42:04
>>198
意味が分からん
理論屋さんでも同じ環境で違う結果が出るのを認めるのは量子論くらいじゃないかな

201 :132人目の素数さん:2005/12/23(金) 11:44:31
>>199
皮肉なのかマジなのかわからん。
計算可能な実数と不可能な実数があって、ルート2は計算可能だそうだ。
いずれにしてもこのスレの本筋からずれている話だとは思うが。

202 :132人目の素数さん:2005/12/23(金) 11:48:15
計算不可能な実数についての議論でさえ、
論理的な議論なら、記号論理に乗せられて、
コンピュータに乗せられるだろう。

203 :132人目の素数さん:2005/12/23(金) 13:20:34
>計算可能な実数と不可能な実数
計算可能ってどういう定義?

そういえば計算可能解析学とかあったね
かなりマイナーな分野だけど鴨さんとかそっち系の分野だったはず

204 :132人目の素数さん:2005/12/23(金) 22:28:15
>計算可能な実数

コーシー列の中でアルゴリズムが定義可能なものの集合、
なんちゃってそんな安直なモノのわけないね(^^)

でもいかにも数学界から相手にされない分野という感じだね。

205 :132人目の素数さん:2005/12/23(金) 22:50:40
>>201,202
「計算不可能」を「計算可能でない」に直したい。

206 :132人目の素数さん:2005/12/23(金) 22:53:35
遅い!

207 :132人目の素数さん:2005/12/23(金) 23:07:22
一つの実数が誕生したと見るためには、
その実数の定義が、有限の長さの、意味の
はっきりした文または式によって記述されて、
しかも、その記述に基いて、その実数の
数値を、任意の精度で有限時間内に算出できる
ことが最低限必要なのだそうだ。
すると、そういう実数は可算個しかないのだ
そうだ。
円周率も、自然対数の底eも、ルート2も、
計算可能な実数であって、確実に「有る」と
言える数なのだと。

208 :132人目の素数さん:2005/12/23(金) 23:16:44
このスレに燃えそうな人と普通の数学屋との間に言葉が
行き交うには、このあたり(チューリングの計算可能な
実数とか)を連結器にするしかないか。いずれの人に
とっても、最大の関心事というわけではないだろうが。

209 :132人目の素数さん:2005/12/24(土) 06:04:25
整数部分をa(0)、n桁目の数字をa(n)としたときに
a(n)が計算可能函数(つまり全域再帰函数でいいんだっけ?)
となること、というのが定義か

でもそういう実数は計算可能というより定義可能とでも行った方が良いんじゃない?

210 :132人目の素数さん:2005/12/24(土) 11:34:05
全ての計算可能でない実数を同一のプログラムで扱うことはできないのは自明だけど
そもそも計算不可能な命題がある事も自明なんだから特に問題はないとおもう

211 :132人目の素数さん:2005/12/24(土) 11:40:02
あれだ。新しい定理の導出は出来るとして

導出できた定理が現在の学会の流行り廃りを考慮した上で価値のある定理かどうかを
AIが判断するのは無理があるだろうな

212 :132人目の素数さん:2005/12/31(土) 19:55:39
世間に媚びる、あるいは相手を持ち上げてその気にさせる、
色仕掛けを使う、おべんちゃらを言う、
こういった知性がAIに備わり、孫氏などの計略をも学べば
危うからず。

213 :132人目の素数さん:2006/01/02(月) 05:35:17
890

214 :132人目の素数さん:2006/01/05(木) 21:47:52
自動証明ソフトが吐き出した証明が1ギガバイトにもなっていたら、
どうやってそれを読んで理解し納得できるというのだろうか?

215 :132人目の素数さん:2006/01/05(木) 21:55:44
四色問題の時にコンピュータで解かせた時にも膨大な結果になったんだよな。
今から25年以上前か…。

216 :132人目の素数さん:2006/01/05(木) 21:56:47
数学者の本源直観によって霊視するのでつ。


217 :132人目の素数さん:2006/01/08(日) 03:41:06
>>192
ゲーデルも、真理に到達するには科学的世界観だけではダメで、神学的世界観も
必要だと考えていたらしい。
来世は存在する。来世が存在しないとしたら今いるこの世界にも意味がないのだそうだ。
この本に書かれていた。
http://bookweb.kinokuniya.co.jp/htm/4535782598.html


218 :132人目の素数さん:2006/01/08(日) 13:40:16
「世界に意味がある」ってなんだろう

219 :132人目の素数さん:2006/01/09(月) 00:46:35
>>217
ゲーデルの考え。

ゲーデル 竹内外史著 日本評論社
pp.178-179
もしこの世界が理性をもって構成されており、意味をもっているとするならば、
来世の再会は存在するにちがいありません。なぜならば、自分自身の発展および
人々との関係に無限の可能性をもっていながら、その千分の一も達成できない
人間という存在を創るということに、いったい何の意味があるでしょうか。
それはちょうど細心の注意と莫大な費用をかけて家の基礎を作り、それからそれを
無駄にしてしまうようなものです。しかし、この世界が理性をもって構成されていると
信ずる理由があるでしょうか? 私はあると信じます。なぜならば、この世界は決して
混乱したものではなく、またどうでもよいというものでもなく、自然科学が示している
ように、いたるところに整然とした秩序があります。秩序というのはまさしく理性の
一つの形態です。

p.183
私は宗教のなかには一般に信じられているよりはるかに多くの理性があると信じています。
もっとも教会のなかにはありませんが。しかしわれわれは若いときから、学校で、
悪い宗教教育によって、また本や経験によって、そうでないと偏見をもつように教育
されています。

220 :219:2006/01/09(月) 00:51:20
>>217
p.184
われわれは来世ではこの世での経験を覚えている。実は来世までは本当にその経験の
意味は理解していない。したがってわれわれのこの世での経験は来世で学ぶための
素材にすぎない。

p.185
もし、この世の経験を来世で覚えていることは不可能だという反対があっても、来世では
潜在した記憶をもって生まれてくる可能性があるということができます。その上、来世では
われわれの心の状態は現世よりはるかによく、したがって来世では、主要なことのすべてを
2×2=4のように絶対に誤らない正確なこととして認識するだろうということを仮定しな
ければなりません。

pp.188-189
私が神学的世界像と呼ぶものは、世界とその内のすべてのものが意味と理性をもっている、
そして正しい疑問の余地のない意味をもっている、という思想です。そしてこの考えは
ただちに次の結論に導きます。われわれのこの世での存在はそれ自身きわめて疑問のある
意味をもっているにすぎないから、それは来世の目的のための手段でしかあり得ない。
さて、この世のすべてのものは意味をもっているという思想は、すべてのものはその原因
をもっているという原理と正確に対応するものです。そしてこの後者の原理はすべての
科学の基礎となっているものです。

221 :219:2006/01/09(月) 00:58:04
>>219-220
竹内氏のコメント
p.178
ここに出てくるゲーデルは私のよく知らないゲーデルである。しかしこれもゲーデルの
一面である。神学や哲学でのゲーデルの考えは私などには分かりかねるが、それでも
彼の数学での考え方といろいろなつながりが認められる。

222 :132人目の素数さん:2006/01/10(火) 00:20:54
ある記号系と公理系を仮定した場合に、
命題Mの証明が可能であるならば、そのような証明のうちで最も
記述が短い証明が存在する。この長さをL(M)としよう。
もしも、ある命題M1に対してその証明があったとして、
仮にその最短な証明の長さL(M1)が10^100とかであったならば、
そのような命題は現実的には書き下すことが出来ないし
(なぜなら宇宙の原子の個数を越えている)、もちろん読み通す
こともできないであろう。10^100ほどではなくても10^10であっても
相当に困難であるが、計算機の容量と速度を持ってすれば格納したり
スキャンしたりすることは可能である。

223 :132人目の素数さん:2006/01/10(火) 00:25:56
逆に云えば、証明が個人の手によるものであるとし、それの理解と確認も
各人が個人として行わねばならないとしたら、L(M)が比較的小さいような
命題Mしか(一生をかけるとしても)現実問題としては取り扱うことが
出来ないのである。一人でやるという立場を放棄して、100人の集団で
分担して証明を書いたり、チェックする、そうしてトップダウン的に
証明のプロセスを分解して部分に分けて、、、と系統的証明が行えるならば
(証明の記述長は幾分長くなるかもしれないが)100人力となり、100倍長い
証明もあるいは検証できるようになるかもしれない、また1万人でなら
1万人力になるかもしれない。しかし人数が増えると次第に誤りが混入する
リスクが高まるので、独立な複数のグループに並行的に検査させたりするほか
本当にチェック機能が働いているかあるいはメクラ判を押していたりしないか
を確かめるためには、わざと証明の一部に誤謬を混入させてそれを検出するか
どうかを二重盲検検査する必要があるだろう。証明行為の過程自身の誤動作
を問題としなければならないからだ。

224 :132人目の素数さん:2006/01/10(火) 00:46:42
そのようなことをしてもせいぜい1000倍とか1万倍とかしか規模を拡大する
ことはできないだろう。さらに数世代に渡って証明を検証するということが
考えられる、代々証明に取り組んで10世代前から取り組んだ検証がまもなく
終わろうとしている、、、、というような具合にだ。
 だが、やはり10^100程度のところに限界があるに違いない。
全数検査しかないような問題であれば、10^100はおろか10^10000のような
問題であっても容易に作れる。
 このような有限行為の立場からは、命題とは何か、証明とは何か、という
疑問が沸いてくる。

225 :132人目の素数さん:2006/01/10(火) 00:56:11
>222
記号系というのは、命題にあわせて拡張されるもので、L(M)のような
関数は大した意味を持たないのではないか。
実際、複雑な数学を多くの人が理解できるようになったのは、記号の
整備によるところが大きいわけだし。

226 :132人目の素数さん:2006/01/10(火) 02:39:20
コンピューターの自動証明を正当化する定理は誰が証明するのだ?

227 :132人目の素数さん:2006/01/10(火) 02:52:21
>>224
先祖が姉歯秀次

228 :132人目の素数さん:2006/01/10(火) 07:58:36
定理の自動証明って
1。恒真式の生成
2。論理変数と事象の結びつけ
に帰着するのでは、、

229 :132人目の素数さん:2006/01/13(金) 03:01:31
素朴な疑問
自動証明をするためには少なくとも体系が決められていなければならない(言語や公理など)。
しかし、数学者はしばしば、新しい対象扱うために、それまで存在しなかった
新しい体系を導入して、そこで考える。そういう体系自体を新たに定義するような行為
は人間にしか出来ないのではないか?

230 :132人目の素数さん:2006/01/13(金) 05:06:14
何でそう思うの?

231 :132人目の素数さん:2006/01/13(金) 12:45:06
ゲーデル&タルスキーによって、次のことが
証明されています:

いかなる数学的問題でも
機械的計算で解決できるような
コンピュータ-プログラムは、
作れない。


232 :132人目の素数さん:2006/01/13(金) 13:33:41
機械的計算じゃない何かをコンピュータに取り入れればできるかもしれない。

233 :132人目の素数さん:2006/01/13(金) 13:59:41
機械的計算しかできないのがコンピュータの特徴付けでは?

234 :132人目の素数さん:2006/01/13(金) 14:08:14
>>230
自動証明が出来るためには(たとえそれが”全て”の証明を網羅できないにしても)
まず体系自体を一つ与える必要がある。
体系を与えればその体系内で成り立つ可算個ぐらいの証明を
自動的に得ることが出来る。
しかし、どう考えてもその課程で、新たな
数学的に興味のある体系そのものが自動的に出てくることは
考えられない。

235 :132人目の素数さん:2006/01/13(金) 14:25:14
>>231
いかなる数学的問題でも解決できる数学者が存在するわけではないし。

236 :132人目の素数さん:2006/01/13(金) 14:52:28
>>234
Aを行う者にBを行うことはできそうもないので、Bを行う者は存在しない?

電卓ソフトで文書作成はできそうもないので、文書作成をするためのソフトは存在しない、とか。

237 :132人目の素数さん:2006/01/13(金) 15:17:20
231のコメントの出自を明らかにしておきます:
文献:前原昭二『数学基礎論入門』朝倉書店

また、ゲーデルの不完全性定理に関するスレッドにも、
関連するコメントがあります。

238 :132人目の素数さん:2006/01/13(金) 15:29:46
文献読むつもりはないが、「いかなる数学的問題」ってのは欲張りすぎ、ってか意味不明だな

239 :132人目の素数さん:2006/01/13(金) 15:39:33
>>238
厳密さを欠いていて申し訳ないです。
『数学的に記述できる問題』
と言い換えればわかりますか?

もっと正確な説明が必要な場合、
やはり不完全性定理を勉強する必要があります。
ここでは長くなりすぎて説明し切れませんので。


240 :132人目の素数さん:2006/01/13(金) 18:35:07
自動証明研究してる人は全員不完全性定理知ってるよ
不動点結合子とか停止性問題とか小テストで出るような基本中の基本だからね

だから誰も「全ての問題の解の列挙」なんて目指してないよ

241 :132人目の素数さん:2006/01/13(金) 21:05:30
例えば代数学の基本定理を証明するために
自然に複素解析の定理を証明するようなコンピューターは作れるのか

242 :132人目の素数さん:2006/01/13(金) 21:44:58
作れない。未定義要素全組み合わせを超える公理系
は作れない。サイコロを振って7の目が出ないことを
証明するようなものだ。

243 :132人目の素数さん:2006/01/14(土) 04:50:28
ちょwwサイコロの例は例えが悪すぎる。
そんなのサイコロを上手く定義して、6つの場合に場合分けして考えれば
証明できるんでは?

244 :132人目の素数さん:2006/01/14(土) 12:18:41
ZFCとかの形式体系における証明に書き直せる証明は
時間が無限にあれば絶対に見つけられるよ。
リウビルの定理を用いた基本定理の証明も当然できる。
効率よく見つける方法は分野の相違に関係なく難しい。
計算機は分野の認識なんかしない。(させようとしなければ)

245 :132人目の素数さん:2006/01/14(土) 13:37:05
>>244
自然数を含む命題論理の成否を決定するアルゴリズムは存在しない。

246 :132人目の素数さん:2006/01/14(土) 16:34:18
>>236
○○作成ソフトの○○が100年後に発見される概念だったら
現時点で○○作成ソフトは作れない。そして○○を発見するという
仕事が数学者に残される。その様な○○はいくらでもありそうなので
数学者の仕事はなくならない、・・・というはなし

247 :132人目の素数さん:2006/01/14(土) 17:34:43
>>246
コンピュータに新しい概念を発見することはできないと思う理由は?
発見できそうもないと>>246が思うから発見できるはずがない?

248 :132人目の素数さん:2006/01/14(土) 19:16:18
>>245
>>244 は定理の集合が帰納的可算だってことを言ってるだけじゃないの?

249 :132人目の素数さん:2006/01/14(土) 20:44:00
新しい概念つってもでてくるのは数字だろ?
それって新しい概念だって人間が見て判断できることなのかね

250 :132人目の素数さん:2006/01/14(土) 21:18:32
>>247
数学的に価値のある体系自体の数え上げが可能ということですか?
そうなると本当に、数学者要らないですね。”独創的”なんていう概念も意味がないことになるし、・・・

251 :132人目の素数さん:2006/01/14(土) 21:23:30
>>つづき
体系そのものをコーディングして(何らかの数を対応ずけて)
数学的に価値ありという概念を式で表して、(これは矛盾しなければ価値ありとしていいのかどうかは良く分からないけど・・・)
その様な数の全体が計算可能かどうかを考えればいいのかな・・・
・・・まあ、どっちの結果にしろ自明じゃないことは分かるわw

252 :132人目の素数さん:2006/01/14(土) 21:26:34
飛行機あるから電車は要らないですね

253 :132人目の素数さん:2006/01/15(日) 16:51:59
有用な定理はこうやって作ると示したとたんに有用ではなくなる不思議。

254 :132人目の素数さん:2006/01/16(月) 10:58:00
『自動証明』の研究では、今、
何が目的ですか?
詳しい人、いらっしゃいましたら、
ご回答願います。

私が少し興味を引かれる問題は、

公理系や取り扱う論理式の全体に、
どのような制約を設ければ、
任意に与えられた論理式が証明可能か
不可能かを機械的に判定できる
アルゴリズムを作れるか?

という問題です。
(興味のない人、ごめんなさいね〜)


255 :132人目の素数さん:2006/01/16(月) 11:04:33
>>219

地球上の人口が増えていくのはどう説明してるんだろう。

256 :132人目の素数さん:2006/01/16(月) 14:28:11
>>255
「人は死んだら生まれかわる」と「人はみな、過去に死んだ人の生まれかわりである」が
違うことは理解しているか?

ついでに言っておくと、ゲーデルは来世が未来の地球だとも未来の"この世"だとも
書いてないよ。

257 :132人目の素数さん:2006/01/16(月) 15:00:40
>>256

とすると、人間には2種類いることになるのか。
生まれかわりとそうでないもの。
不公平だなw

>ついでに言っておくと、ゲーデルは来世が未来の地球だとも未来の"この世"だとも
書いてないよ。

書いてないけど文脈からそうとしか思えない。

258 :132人目の素数さん:2006/01/16(月) 15:36:54
来世は人大杉だな

259 :132人目の素数さん:2006/01/16(月) 16:46:25
仮に我々が生まれ変わりだとしても前世の記憶がないっていうのは
致命的だな。これじゃ生まれ変わりだろうがそうでないだろうが
実質同じこと。

260 :132人目の素数さん:2006/01/16(月) 18:05:57
そこで江原さんですよ

261 :132人目の素数さん:2006/01/16(月) 22:38:27
過去に同じ遺伝子構造を持っていた人間が存在した場合に生まれ変わりとなる

262 :132人目の素数さん:2006/01/17(火) 09:00:51
一卵性の双子の兄は俺と同じ遺伝子構造を持っているのだが
俺は兄の生まれ変わりなのか

あと、クローン人間禁止されたら俺は殺されるのか

263 :132人目の素数さん:2006/01/19(木) 03:46:05
>>245
自然数があるのに命題論理とは・・・。
248の言うとおり、REだと言っているだけだよ。
いい加減な知識に基づいて考えるのは危険だよ。

264 :132人目の素数さん:2006/01/22(日) 03:41:20
>>263
OMOIKOMI NO HAGESHII YATSUYONOO

265 :132人目の素数さん:2006/01/22(日) 22:57:18
age

266 :132人目の素数さん:2006/01/23(月) 22:48:57
>>264
仰るとおり。ごめん。244は誤り。

267 :132人目の素数さん:2006/01/24(火) 09:42:34
coqとか使ってる?

268 :132人目の素数さん:2006/01/29(日) 05:19:47
この手の問題の解決の糸口になりうるものは、
近年再び盛んになった人間の脳の機能や構造の研究であろう。

数学を行う作業を、脳の活動をリアルタイムでモニタリングする
帽子をかぶりながら、知的作業に対して脳が如何に使われるかを研究
するのである。おそらく、代数学と幾何学では使われる部位が
違っているとか、そういう類の発見とか、あるいはある事柄
を抽象化したり一般化したりする脳の機能の解明の糸口が
みつかるかもしれない。さらに、頭蓋を外してここだとめぼしを
つけた部位に電極をさして、。。。。。
 そのようにして、脳の推論する機能が段々よく分かってきたら、
あるとき偉大な者が現われて、脳シミュレータを開発し、ついに
プログラムによらない自己学習型、自己発見型、自己推論型の
人工数学者ができるかもしれない。彼は外界の情報をネットと
電子ライブラリーを参照しながら、ただもくもくと数学にいそしむ
のである。世間はこのシステムの完成をみて、もはや数学者は要らない
と短絡的な意見に走り、数学者を野に放って数学以外の労働を
強制するかもしれない….

269 :132人目の素数さん:2006/02/05(日) 07:27:08
281

270 :132人目の素数さん:2006/03/02(木) 16:59:59
367

271 :中川泰秀 ◆IvNr9.tOCg :2006/03/13(月) 16:40:57
数学が正しい事を自動で証明して見よ

272 :132人目の素数さん:2006/03/14(火) 04:35:18
age

273 :132人目の素数さん:2006/03/14(火) 14:46:41
コンピュータは自分自身が正しいことを証明できない。
証明しようとすると、必ず自己矛盾か無限ループに落ちるから
考えないようにしている。自己のことを考察した瞬間に
システムのどこかに必ず不動点が生じて、そこで引っかかって
抜けて来れなくなるのだ。

274 :中川秀泰 ◆IPeKUwqiHM :2006/03/14(火) 14:50:55
仲々良い所を付いているじゃないか
これはコンピューターばかりでなく人間にも当てはまる。

275 :BW of Tama King:2006/03/14(火) 14:54:52
>>274 キングに証明させるのがよかろう。
奴は数学の召喚獣スクリプトだから。 普通あんなけレス出来んぞ。
キング無理すんなよー オーバーヒートするぞぉー

276 :GiantLeaves ◆6fN.Sojv5w :2006/03/14(火) 15:00:04
talk:>>275 私を呼んだか?

277 :BW of Tama King:2006/03/14(火) 15:01:30
>>276 呼んだよ? 数学が正しい事を自動で証明して見よ だって。


278 :中川秀泰 ◆IPeKUwqiHM :2006/03/14(火) 15:07:02
◆6fN.Sojv5w
等というking見た事無し


279 :GiantLeaves ◆6fN.Sojv5w :2006/03/14(火) 15:36:00
talk:>>277 では数学とはどのような命題か?
talk:>>278 何だよ?

280 :BW of Tama King:2006/03/14(火) 15:45:12
>>279 中川さんに聞け。

281 :132人目の素数さん:2006/03/26(日) 14:29:19


282 :132人目の素数さん:2006/04/04(火) 22:11:13
このスレもう終わりか?

283 :132人目の素数さん:2006/04/15(土) 23:09:20
193

284 :中川秀泰:2006/05/12(金) 05:31:36
どうせ哲厨のスレだから終わりにして良い

285 :132人目の素数さん:2006/05/13(土) 22:25:06
521

286 :132人目の素数さん:2006/05/14(日) 05:01:34
どうせなら形式化された証明のデータベースの話とかしたいな。

287 :132人目の素数さん:2006/05/16(火) 15:42:02
MIZAR!

288 :132人目の素数さん:2006/05/16(火) 16:04:34
定理の自動証明ってMathematicaとPrologで既に商品化されてるよな

289 :132人目の素数さん:2006/05/26(金) 14:14:49
620

290 :132人目の素数さん:2006/06/16(金) 01:05:04
912

291 :132人目の素数さん:2006/07/28(金) 15:37:13
977

292 :132人目の素数さん:2006/08/15(火) 04:09:52
あ   あ   あ   あ     あ     あああああ
あ  あ    あ   ああ    あ    あ     あ
あ あ     あ   あ あ   あ   あ       
ああ      あ   あ  あ  あ  あ     あああああ
あ あ     あ   あ   あ あ   あ      あ
あ  あ    あ   あ    ああ    あああああああ
あ   あ   あ   あ     あ          あ


あ              あ
あ            あああああ
あ              ああああああ
あ     あ       ああ     あ
あ     あ      あああ    ああああ 
あ    あ      あ  あ   あ あ
 ああああ          あ    あ 

293 :KingOfUniverse ◆667la1PjK2 :2006/08/17(木) 06:00:12
talk:>>292 人の脳を読む能力を悪用する奴を潰せ。

人の脳を読む能力を悪用する奴を潰せ。

294 :132人目の素数さん:2006/08/30(水) 16:55:54
648

295 :132人目の素数さん:2006/10/03(火) 00:21:38
174

296 :132人目の素数さん:2006/11/12(日) 23:47:29
968

297 :132人目の素数さん:2006/12/07(木) 20:24:25
自動証明の研究に、何の価値があるの?

298 :132人目の素数さん:2006/12/07(木) 20:38:28
>>297
なぜ出来ないか考えるきっかけになる。

299 :132人目の素数さん:2006/12/07(木) 20:52:47
こらっつぐらいからやれば何がネックかわかるよ。

300 :132人目の素数さん:2006/12/07(木) 21:30:46
こらっつって3x+1と.5xをコンフォーマルマップで2つの
円のあいだの領域に飛ばして、グラフが1に収束する力学系を
つくればいいんでしょ?

301 :数学系のD1です:2006/12/07(木) 21:43:09
>299

ありがとうです

302 :132人目の素数さん:2006/12/07(木) 23:13:55
f(z)=arg(z-p0)e^2π(1/(1+1/|z-p0|))i
は直線を同心円にマッピングする。


303 :132人目の素数さん:2006/12/07(木) 23:41:34
f(z)=arg(z-p0)e^2π(1-1/(1+|z-p0|))i
は直線を同心円にマッピングする。

304 :132人目の素数さん:2006/12/07(木) 23:42:34
こらっ

305 :132人目の素数さん:2007/01/01(月) 00:05:23
↓うるせーんだよ
↓このスレを見ている人はこんなスレも見ています。(ver 0.20)

306 :132人目の素数さん:2007/02/05(月) 17:08:31
610

307 :132人目の素数さん:2007/02/07(水) 04:18:00
それより証明を形式的に記述して検証する方法に興味がある

308 :132人目の素数さん:2007/02/07(水) 05:05:15
思考とは組合せ探索なり。

309 :132人目の素数さん:2007/02/07(水) 11:50:21
コンピュータで数万年かかるような組み合わせから
最適(に近いもの)を一瞬で見つけられるのはなぜなんだぜ?

310 :132人目の素数さん:2007/02/07(水) 21:31:58
きっと将棋のプロと同じ原理だよ

311 :132人目の素数さん:2007/02/08(木) 06:28:03
>>309
逆もあるよん

312 :132人目の素数さん:2007/02/10(土) 18:55:12
人間の場合超自然的な予見ができるから

313 :132人目の素数さん:2007/02/11(日) 13:27:43
人はそれを「当てずっぽう」と呼ぶ。

73 KB
■ このスレッドは過去ログ倉庫に格納されています

★スマホ版★ 掲示板に戻る 全部 前100 次100 最新50

read.cgi ver 05.02.02 2014/06/23 Mango Mangüé ★
FOX ★ DSO(Dynamic Shared Object)