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

コンピューターによる ..

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に備わり、孫氏などの計略をも学べば
危うからず。

次ページ