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

これが可能になったら数学者という仕事が無くなっちゃうの？

2

定理の自動証明が実用レベルに達してるなら他の大抵の仕事も実用レベルに達する。
その時にコンピュータには出来ないような新しい仕事を見つけられなければ
数学者だけでなく殆どの人間の仕事が無くなる。

で、
コンピュータによる定理の自動証明ってどうやるのさ？

趣旨とは違うが、「A=B」のような方向はもう少し発展すべきだと思う。

ゲーデルの考えが正しいとすると、機械には数学者と同じレベルの証明は、
永久に出来ないだろう。

>コンピュータには出来ないような新しい仕事
何が「美しい」か見極める事(新しくないけど)。
コンピュータの万能性の可能性を否定するにはそれだけで十分。

主観がない、ということか。

数学の概念を全て「記号」であらわすというのはライプニッツの目指したもの。
それを2進であらわせれば、コンピュータに数学をやらせる土台ができるかもな〜。

可能にはなると思うが、
「美しい証明」になるかどうかは別問題。

既にある証明のデータベース化は進んでないの？自動証明による証明の再現という意味なのだけど。

意味が概念として理解できなければ組合せの爆発により証明が終了しない。

数学にも哲学にも通じてる情報科学のあったまぃー人が解決してくれるんでしょ

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

四色問題か

>>15
たしか、二等辺三角形がどうたらってやつだった
四色問題は異論があるから微妙じゃない?

４色問題は、地図を幾つかのパートに分割して、
その全てのパートに対して定理が成り立つことを確認する所を
コンピュータにやらせたんだったっけ？
この場合、コンピュータは人間の作ったアルゴリズム通りに動作しているだけなので、
「自動」証明とは言い難いなぁ。
てか、自動証明って何？コンピュータが1から全部証明やってくれることでしょ？

四食問題は単に機械的にチェックできる部分をやらせただけなのでは。
微分方程式の数値解を計算機で出すか手計算でやるかの違いみたいな感じがする。

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

定理の自動証明は公理から出発して定理が導けるまで動作を続けるか、
定理から証明に必要な公理を導き出す。

>>19
基本的には¬（公理⇒定理）から自動的に矛盾を導く。
証明が存在するなら、矛盾が導ける。
しかし、存在しない場合にはプロセスが終了しない可能性がある。

>>20

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

「こういうときにはこの定理を用いる場合が多い」っつー傾向というのがありまして、
そういうメタ知識を用いると、かなりよくなります。

>>22

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

>>23
なんじゃそりゃ、
もしや0から全てコンピュータに行わせようとしてるのか？
過去の資産を生かさずしてどうする。

いつまでも人間が面倒みなけりゃならないなら、こっちこそなんじゃそりゃ
と言いたくなるな

コンピュータは所詮道具なんだよ。
人間がやる定理証明に役立ってくれればいいの。
なんでもかんでもコンピュータにやらせる必要は無いの。

とりあえず定理のデータベースを作ってくれ。

>>5
A=B？

>>26
それで役立つんかい？
人間が証明出来ない定理をコンピュータが証明してくれるとか？

>>1
正しい定理を見つける仕事は残るだろう。

ときたまジョブをチェックする仕事は必須

人間に証明出来ない問題がコンピュータに証明出来るわけないわな。
コンピュータなんてただ計算が速いだけだし。難しい予想なんて解こうものなら既存の数学では無理な場合もあるし、
コンピュータがその道具を作っていくなんてまず不可能じゃね？

人間だろうがコンピュータだろうが鼠を取るのが良い猫だ。

コンピュータに快楽と苦痛を与えればなんでも出来る。

オダインに頼め。
エルオーネの能力に比べれば、証明なんて

>>34
強化学習も結局はx^nオーダーの計算量となるわけで

追試・データベース化、翻訳などに役立つであろう。

合流性とか停止性とかいう話があったよね＞証明系

おまえらPrologは知ってるよな？

ああ、あの失敗したプロジェクトで使われた言語ね
第五世代コンピュータ開発計画とかいう税金のムダ使いで

プログラミング言語で一種のファッションだろ？

プログラミング言語は流行廃りが激しいから、数学者が勉強すべきものではないだろう。

自動証明⊆人工知能
と言える？
人間並みの人工知能ができれば、自動証明もできるはず。

証明作成のアルゴリズムとして、どんな方法がありうるのか？
検索の枝きりが難しいと思う。

あ、今アリゴリズム体操おわっちゃった。

こっち向いて二人で前ならえ
あっち向いて二人で前ならえ

>>28
> >>5
> A=B？
ググれ。

>>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

ﾊｧ?

ほらAIってあれだろっ！ドラクエ４に搭載の…

ボスに向かってザラキを唱えるやつか。

>>48
キミはgoogle の使い方を知らない。

この分野は日本では信州大が一番進んでいる
ようだよ。
お前らが大好きな数研の教科書書いてる方が
精力的に進めている

>>52
mizarは"theorem prover"ではなく"proof checker"ですよ。
checkerでさえ現状ではライブラリ不足で実際に数学では使えないでしょう。

>>51
ではどのようにすればA=BでGoogleで検索できるか教えていただけますか？

(´-`).｡ｏO(二重引用符でくくれとかそういうｵﾁかな？)

挑発したら教えてもらえなくなるよ

はいはいヽ(´ー`)ﾉ

>>53
ライブラリ不足かどうかは知らんが、そもそも現実の数学研究で使えるような
表現力を持つ言語を処理させるのはきついんじゃなかろうかと思う。

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

コンピュータにPeano算術での自動証明プロセスを与えて、
しらみつぶしで¬(0=0)の証明を探索させたら、
もしかしたら有限時間内に「証明あり」って出力が返る可能性がある?
もしそうなったらどうなるの?

>>58
PA が矛盾してるならあるかもね

>>59
こえー。そしたら帰納法使った証明が全ておじゃんだしZFとかも壊滅だし。
>>58の自動証明を延々走らせてる不信心な暇人っていないのかな。

A=B 等式証明とコンピュータ, 1997 トッパン
トッパンが2000年に出版事業から撤退したため、あまり知られてない。
幸い原本がpdfで公開されている。クヌースによる序言だけでも読むことを勧める。

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

>>21
＞それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
人間もバカチョンでしらみつぶしに探してる。意識してないだけ。

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

>人間もバカチョンでしらみつぶしに探してる。意識してないだけ。

嘘だろ

>>63
残念だが本当だ。
ところで、誰かTarskiの量化記号消去について簡単に説明してくれ。

>>64

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

>>65
いや、そのくらい時間がかかるのが当然なんだ。
それより、質問したことについて知らないなら黙っててくれ。
無知な奴と遊んでる暇はないんだ。

>>66

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

>>67
＞現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。

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

>>68

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

彼の「しらみつぶし」って単語の定義が俺様独自定義なんだろ

昔の人がすでにしらみつぶしに調べてきたから今の人はそうする必要がないという理屈だな

例えば将棋で次の一手をしらみつぶしで探せるはずがない。
それと同じで証明もこうすればよさそうだ、とある程度見切りをつけて行っているはず。
直観力+構成力+知識・経験が物を言う。

>>71

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

>>72
我々がそういう力を持ってるのは昔の人がしらみつぶしにやって得た知識を
受け継いでるからだと考えることもまったく不可能なわけではないんじゃない？

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

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

コンピュータで証明するときに、あらかじめ「知識」のデータベースを入れて
それ使って証明しても「しらみつぶしで証明しました」って言うわけか？

しらみつぶしって言うのは、たとえて言うなら、10回戦のトーナメント方式の1回戦から全ての対戦を行うことに例えれば。
知識があるっていうのは、経験則でこの対戦は無いってシードの部分がいくつかあって考慮する必要のない部分があるってことでしょ。

今使ってるパソコンでも、π=3.14・・・とかはいちいち計算しないで使われてるんだろ？

意味を理解しているならばしらみつぶしに探索しなくてよい。

おまえら、せめてヒューリスティックスって言葉使えよ・・・

うむ、そういえばそんな言葉があったな。
最近使ってなかったせいか忘れていた。

>>77
ヒューリスティックスなしらみつぶしで、「知識」のデータベースを
元に計算してまつ

>>81
ﾜﾛｽw

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

書き込んでる最中に暗殺された>>83のご冥福をお祈り致します。

>>72
＞証明もこうすればよさそうだ、ある程度見切りをつけて行っているはず

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

>>83-84
ﾜﾛｽw

＞人間の知能の仕組みなんて誰もなーんもわかっちゃいない。
＞それをコンピュータでシミュレート出来るわけがない。

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

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

>>87

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

>>88
不思議とは無理解のことである。

この場合は無理解というより不可解

地球の原子すべてをシミュレーション出来るコンピュータが出来たら生物はもちろん文明さえもシミュレーション
出来るのではないか。

>>91

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

>>91
そのコンピュータは自分自身をシミュレートするのか？

哲学的な問いでなかなか面白いでつね。

>>94　
チューリングマシン
とか
停止問題
でぐぐってみ。否定的な結論が出るから。

証明すべき命題をどう符号化するか、という問題がまずある。
もし、すべての数学定理が計算機で証明できるならば、
たったひとつのアルゴリズムから、次々に定理を自動生成できるんじゃなかろうか？
そんなアルゴリズムが果たして存在するのか？

>>96
ZFC を計算機で書けばいいわけだから原理的には余裕でできる
けどなんか工夫しないと時間かかりすぎて意味のある定理はほとんど出ないと思う

>>96
くそ定理は山程合成出来る。

人間機械論を否定したゲーデルの論文があると聞いた。
彼の不完全性定理を基にしている。
人工知能を研究している人なら知ってるよね？

>>93
コンピュータをシミュレーションするコンピュータはターゲットのコンピュータより
メモリは大きくスピードも速くなければならない。

そんなことより地球シミュレータのデータのほうが問題だろ。
全ての原子のデータなんてわかるわけがない。
可能性があるとしたらBig Bangのシミュレータ。
仮に出来たとしても地球が出来るまで相当時間がかかるｗ

>>100
確かにメモリは大きい必要があるが、
スピードに関しては遅くても構わない。
ただし、もちろん実物より遅くなってしまう。
用途によっては実物より遅くても、結果の再現が得られれば良い場合もある。
例えば新しいCPUの回路設計など。

>>98
文字通りトリビアの泉になるわけだな……。

山田君、座布団1枚もっていki（略

停止性問題しかり、ﾃﾞｨｵﾌｧﾝﾄｽ方程式しかり、計算機で証明できない問題はたくさんあるわけで。
「定理」は有限文字列で表現できるから
「この世のすべての定理」を列挙することは一応できるけど
それらすべての真偽を判定することはできないと言うことか。

>>105
証明できないものを定理とは呼ばないんじゃ？
それでも定理全てを列挙することは出来るが。

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

>>106
ゴメンナサイ。「定理」ではなく「命題」と言うべきでした。

一応確認すると、定理全体の集合は recursively enumerable ですよね？

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

>>108
どんまい

>>109
そうだよ

そうですよね。
>>105を見るとそうでないように読めたので気になったので。

あれ、そうでないように読めたのが勘違いか。
有限時間内に真偽を判定することはできませんね。
どうもすいません

>>110
高校数学の本閲覧したけど…１社だけ、JavaScriptだなｗ
確かに、関数型を通り越して、オブジェクト指向言語だわ。
で、こんなの勉強していちいち

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

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

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

情報科学の人も、プログラミングできる人の方が少数派なんでしょ？

>>112
r.e.だけだと偽かどうかを判定する手続きが止まらない可能性があるから
そういう意味では真偽を判定出来ないとも言える。
decidable(=recursive)ではないってことだ。

>>114
＞高校数学の本閲覧したけど…１社だけ、JavaScriptだなｗ
マジ？！！
これで勉強させられるヤツら悲惨だな…。
本質的でない部分が多く含まれる上に、どうせ教える側も良くわかってないんだろうし。

>>117
まともな、高校数学教師なら、その教科書のその部分は「飛ばすべき」だ。
後で、校長や教頭から文句がくるやも知れないが、その方が「良心的」だと思う。

>>110
Ｃ言語でLispコンパイラを書けばいいじゃないか。

>>119
コンパイラを書くと何がいいの？

>>105
>「この世のすべての定理」を列挙することは一応できるけど

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

>>99
>人間機械論を否定したゲーデルの論文があると聞いた。

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

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

人間機械論は人間と機械論が正しいと聞いたが、

それはどうでもよくて、>>122のゲーデルの趣旨は、人間の頭脳は
チューリングマシンのような機械ではないということ。

>>122
>不完全性定理は機械には証明できない

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

確かに人間の脳はチューリングマシンと違うよね。もしかしたらチューリングマシンにノイズの項を追加すると人間の脳と等価になったりして。ゲーデルはきっとノイズが大嫌いだよね（独断と偏見）。

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

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

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

ある種のノイズが関係していることは十分考えられる。
量子力学的ゆらぎとか。
そのノイズによりひらめきが誘発されるとか。

>>不完全性定理は機械には証明できない
>自分で言い出してなんだけど、これ本当かな。
もちろん初歩的な誤り。
不完全性定理は形式的証明が可能。
証明できないのはゲーデル命題。
もっとも、人間にも証明できないわけだが。

例えば、三角形の定義を入力すると三角形に関するありとあらゆる定理（クソなのも含めて）を生み出す
ってことは出来るのかな？

公理や推論規則も入力すればできる

初等幾何の証明はどうするんだろう。
図は別に使わないだろうけど、補助線の考え方自体は要るよね。
あれは激しくセンスが必要な気がするんだが…。

・・・え？

ところで、数学の定理って有限？

夢幻

>>132
適当に総当たりで補助線引いてみて、過去の定理を当てはめることができるか、
総掛かりで検索する…とか。

>>134
家産

>>132
証明の方法まで指定するのか？
コンピューターで計算するんなら、座標やベクトルを使うことになるんじゃないのかな。

＊ 任意の命題を証明するアルゴリズムは無い。

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

問題：
数学的帰納法で証明できる自然数の定理は、
すべてコンピュータで自動証明できるか？

Ｎｏ　かな？

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

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

Ｙｅｓだな！

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

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

人間だって有限時間で全ての定理を証明する事はできないジャン

>>143
人間ならできる！といった覚えは一度も無いが

帰納法使えばいいじゃない

>>139
それは命題を入力として証明手続きを列挙する手続きの存在を仮定してるから
結局同じことなんだが。
あと真でない命題を入力した時に有限時間内に終わらない可能性がある。
最終行の可算は有限の間違い？

いや、ちょっと架空の話で例示してみよう。
（本当はこういうことはないのだが、N文字で書かれた任意の命題を
証明することのできる・あるいは否定できる手続きのプログラムで
１０＾１０＾N文字以内で書けるものが常に存在する、
というようなことがあったと仮にしてみよう。もちろん嘘だが）
もしもそうであれば、
そのとき、ある任意の命題（その長さをN文字としよう）
が与えられたとして、それから始めて、１０＾１０＾N文字以内の
プログラムをすべて列挙して調べれば原理的には答えがわかる
ということになる。

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

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

295 ：１３２人目の素数さん ：2005/09/29(木) 11:58:46
夫馬です。

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

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

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

土建屋、宇沢、長谷川、黒木の数理物理、可積分系、表現論自体が
コケオドシだから、黒木にこいつらを叩く資格はないよｗ

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) に近い穏健だが当たり前の主張を述べて批判をかわします。
http://www.math.tohoku.ac.jp/~kuroki/FN/relativism.html

552

記号論理学が嫌われるのは、命題という、数のようにモノと思いやすくない
ものまでＡとかＢとかいう記号で扱うことに対して、無意識の不安、抵抗
があるからであろう。
これを払拭させるには、まず。「命題はモノではない」ということを
明確に意識させたうえで、「それでも命題は或る意味でモノ扱い出来る」
ということを相当徹底的に理解させることが有効であろう。

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

そのあで　ー＞　そのあとで

>>152
そういった内容は認知心理学でいうメタ知識に相当するから、
いわば「公理の公理」としておさえておくことが好ましい。

記号論理学の見た目の記号がつまらん。

記号論理学って嫌われてるのか？
どういう人に？

大統一数学理論ってないですかね。

人間の脳みそで出来るんだからコンピューターにだって出来るだろ

今のコンピュータじゃかなり難しいだろ

出来たとき有益で人々から感謝されるならば作る価値がある。

不完全性定理の証明とか見るとわかるが
コンピュータに足りないのは定義を増やすという操作なわけだよ

age

定義を増やすぐらい出来ているが・・・

融通が効くかどうかが重要なのね

924

コンピュータが出来てから１０年くらいたったころだから今から
５０年位前に計算機科学の有名な学者が１０年以内に定理の
自動証明が出来るだろうと予言した。だから専門家といってもなーんも
分かってないんだよ。現在だって同じ。

しらみつぶしに証明のゲーデル数が小さい方から
定理を全て証明していくつもり、、だったんだろうかな
何の見積もりを間違えたんだろう？
実際の定理の複雑さか計算機のスピードか

ノイマン式コンピュータじゃ無理だろ。
ま俺は専門家じゃないからあてにならないがｗ
今のコンピュータというのは原理的には５０年前と同じ、
つまりノイマン式。これをいくらいじっても無理だろう。

四色問題はチェック作業を機械化しただけであり、自動証明とは言えない。
しかし証明に携わった人間によれば、時折コンピュータが
人間以上の「知性」を垣間見せることがあるという…。

>>169

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

Kingって結構チューリングテストに合格しなかったりしてｗ

ってか自動証明の話してるときにチューリングテストの話せんでもいいだろ

talk:>>171 何やってんだよ？

いやいかにも
talk:>>とか自動生成っぽいなとか思ってｗ

>>172

冗談通じないのね。

定理の自動証明なんて散々研究されてる分野なんだが
なんで出来ないとか主張してる奴がいるんだ？

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

age

>なんで出来ないとか主張してる奴がいるんだ？

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

研究されてるのと、実際に実現してるのは別だよね
AIも然り

コンピュータのスピードさえ上がればえらいことになるだろ？
暗号だけじゃなくて定理証明も。
量子コンピュータとかが実用化したら、、、？

そうかなあ、、結構オーダーが違うと思うけど、、
第一コンピューターがそんなに早かったら
気象学も分子生物学も量子化学も今より進歩してるはずだよw

１８１の２行目以降は無意味。

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

人間の脳だって化学反応の連鎖で動いているだけだけどな

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

＞証明された定理のうち、人間にとって意義あると思われる
＞ものを選び出すのは人間の仕事となるだろう。
そんな100億（くらい少なけりゃまだ良いがｗ）の芥の中から
1個の宝石を選び出す仕事が成立すると思うのかねｗ

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

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

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

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

＞でもコンピューターでは有限の数しか扱えないので無理数は扱えない。
代数的数なら頑張れば扱える気がするけどね
扱い方工夫すれば

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

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

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

コンピューターで扱っているのは有限の２進数だから
近似値としての無理数以外扱えない。無理数の近似値
は有限の数、すなわち有理数のなかで有限のものだけ
しか正確には扱えない。これで様子を調べるとか近似値
を求めることはできる。科学実験ではそれで十分かも
しれないが数学はそういう立場ではないでそ。

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

人間にとって有益な定理は複数の命題から単純な命題を導き出すからコンピューターの糞定理からそんな形式を抜き出せば
比較的簡単に見付かる。

>>189
修正。「記号論理の原理」じゃなくて「記号論理の効用」
原理は別にある。
>>191
そう言う次元の話じゃないの。「記号論理の原理」について
１０冊ぐらいの本で１０ヶ月ぐらいかけて考えてくれ。留年
覚悟で。尤も、本人に時期が来てないなら、それでも分らん
だろうが。
分らなくてもいい。走りの原理が分らなくても走れれば
素晴らしいから。

無理数の話
＞ttp://www.gakushuin.ac.jp/~881791/d/0508.html#15

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

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

数学は？

？

>実験環境を整えてある実験をしたところ99回とも同じ、面白い結果が出た
同じ実験をして違う結果がでると実験屋さんたちは認めないんでしょ。
数学の反例みたいなもんで。現実はわからんのをいいことに捏造なんか
もあるかもしらんが。

2^(1/2)

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

>>198
意味が分からん
理論屋さんでも同じ環境で違う結果が出るのを認めるのは量子論くらいじゃないかな

>>199
皮肉なのかマジなのかわからん。
計算可能な実数と不可能な実数があって、ルート２は計算可能だそうだ。
いずれにしてもこのスレの本筋からずれている話だとは思うが。

計算不可能な実数についての議論でさえ、
論理的な議論なら、記号論理に乗せられて、
コンピュータに乗せられるだろう。

＞計算可能な実数と不可能な実数
計算可能ってどういう定義？

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

＞計算可能な実数

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

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

>>201,202
「計算不可能」を「計算可能でない」に直したい。

遅い！

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

このスレに燃えそうな人と普通の数学屋との間に言葉が
行き交うには、このあたり（チューリングの計算可能な
実数とか）を連結器にするしかないか。いずれの人に
とっても、最大の関心事というわけではないだろうが。

整数部分をa(0)、n桁目の数字をa(n)としたときに
a(n)が計算可能函数（つまり全域再帰函数でいいんだっけ？）
となること、というのが定義か

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

全ての計算可能でない実数を同一のプログラムで扱うことはできないのは自明だけど
そもそも計算不可能な命題がある事も自明なんだから特に問題はないとおもう

あれだ。新しい定理の導出は出来るとして

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

世間に媚びる、あるいは相手を持ち上げてその気にさせる、
色仕掛けを使う、おべんちゃらを言う、
こういった知性がAIに備わり、孫氏などの計略をも学べば
危うからず。

890

自動証明ソフトが吐き出した証明が１ギガバイトにもなっていたら、
どうやってそれを読んで理解し納得できるというのだろうか？

四色問題の時にコンピュータで解かせた時にも膨大な結果になったんだよな。
今から２５年以上前か…。

数学者の本源直観によって霊視するのでつ。

>>192
ゲーデルも、真理に到達するには科学的世界観だけではダメで、神学的世界観も
必要だと考えていたらしい。
来世は存在する。来世が存在しないとしたら今いるこの世界にも意味がないのだそうだ。
この本に書かれていた。
http://bookweb.kinokuniya.co.jp/htm/4535782598.html

「世界に意味がある」ってなんだろう

>>217
ゲーデルの考え。

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

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

>>217
p.184
われわれは来世ではこの世での経験を覚えている。実は来世までは本当にその経験の
意味は理解していない。したがってわれわれのこの世での経験は来世で学ぶための
素材にすぎない。

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

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

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

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

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

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

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

コンピューターの自動証明を正当化する定理は誰が証明するのだ？

>>224
先祖が姉歯秀次

定理の自動証明って
１｡恒真式の生成
２｡論理変数と事象の結びつけ
に帰着するのでは、、

素朴な疑問
自動証明をするためには少なくとも体系が決められていなければならない（言語や公理など）。
しかし、数学者はしばしば、新しい対象扱うために、それまで存在しなかった
新しい体系を導入して、そこで考える。そういう体系自体を新たに定義するような行為
は人間にしか出来ないのではないか？

何でそう思うの？

ゲーデル&タルスキーによって、次のことが
証明されています：

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

機械的計算じゃない何かをコンピュータに取り入れればできるかもしれない。

機械的計算しかできないのがコンピュータの特徴付けでは？

>>230
自動証明が出来るためには（たとえそれが”全て”の証明を網羅できないにしても）
まず体系自体を一つ与える必要がある。
体系を与えればその体系内で成り立つ可算個ぐらいの証明を
自動的に得ることが出来る。
しかし、どう考えてもその課程で、新たな
数学的に興味のある体系そのものが自動的に出てくることは
考えられない。

>>231
いかなる数学的問題でも解決できる数学者が存在するわけではないし。

>>234
Aを行う者にBを行うことはできそうもないので、Bを行う者は存在しない?

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

２３１のコメントの出自を明らかにしておきます：
文献：前原昭二『数学基礎論入門』朝倉書店

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

文献読むつもりはないが、「いかなる数学的問題」ってのは欲張りすぎ、ってか意味不明だな

>>２３８
厳密さを欠いていて申し訳ないです。
『数学的に記述できる問題』
と言い換えればわかりますか？

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

自動証明研究してる人は全員不完全性定理知ってるよ
不動点結合子とか停止性問題とか小テストで出るような基本中の基本だからね

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

例えば代数学の基本定理を証明するために
自然に複素解析の定理を証明するようなコンピューターは作れるのか

作れない。未定義要素全組み合わせを超える公理系
は作れない。サイコロを振って７の目が出ないことを
証明するようなものだ。

ちょwwサイコロの例は例えが悪すぎる。
そんなのサイコロを上手く定義して、6つの場合に場合分けして考えれば
証明できるんでは？

ＺＦＣとかの形式体系における証明に書き直せる証明は
時間が無限にあれば絶対に見つけられるよ。
リウビルの定理を用いた基本定理の証明も当然できる。
効率よく見つける方法は分野の相違に関係なく難しい。
計算機は分野の認識なんかしない。（させようとしなければ）

＞＞244
自然数を含む命題論理の成否を決定するアルゴリズムは存在しない。

>>236
○○作成ソフトの○○が１００年後に発見される概念だったら
現時点で○○作成ソフトは作れない。そして○○を発見するという
仕事が数学者に残される。その様な○○はいくらでもありそうなので
数学者の仕事はなくならない、・・・というはなし

>>246
コンピュータに新しい概念を発見することはできないと思う理由は?
発見できそうもないと>>246が思うから発見できるはずがない?

>>245
>>244 は定理の集合が帰納的可算だってことを言ってるだけじゃないの？

新しい概念つってもでてくるのは数字だろ？
それって新しい概念だって人間が見て判断できることなのかね

>>247
数学的に価値のある体系自体の数え上げが可能ということですか？
そうなると本当に、数学者要らないですね。”独創的”なんていう概念も意味がないことになるし、・・・

>>つづき
体系そのものをコーディングして（何らかの数を対応ずけて）
数学的に価値ありという概念を式で表して、（これは矛盾しなければ価値ありとしていいのかどうかは良く分からないけど・・・）
その様な数の全体が計算可能かどうかを考えればいいのかな・・・
・・・まあ、どっちの結果にしろ自明じゃないことは分かるわｗ

飛行機あるから電車は要らないですね

有用な定理はこうやって作ると示したとたんに有用ではなくなる不思議。

『自動証明』の研究では、今、
何が目的ですか？
詳しい人、いらっしゃいましたら、
ご回答願います。

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

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

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

>>219

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

>>255
「人は死んだら生まれかわる」と「人はみな、過去に死んだ人の生まれかわりである」が
違うことは理解しているか?

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

>>256

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

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

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

来世は人大杉だな

仮に我々が生まれ変わりだとしても前世の記憶がないっていうのは
致命的だな。これじゃ生まれ変わりだろうがそうでないだろうが
実質同じこと。

そこで江原さんですよ

過去に同じ遺伝子構造を持っていた人間が存在した場合に生まれ変わりとなる

一卵性の双子の兄は俺と同じ遺伝子構造を持っているのだが
俺は兄の生まれ変わりなのか

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

>>245
自然数があるのに命題論理とは・・・。
248の言うとおり、ＲＥだと言っているだけだよ。
いい加減な知識に基づいて考えるのは危険だよ。

>>263
OMOIKOMI NO HAGESHII YATSUYONOO

age

>>264
仰るとおり。ごめん。２４４は誤り。

coqとか使ってる？

この手の問題の解決の糸口になりうるものは、
近年再び盛んになった人間の脳の機能や構造の研究であろう。

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

281

367

数学が正しい事を自動で証明して見よ

age

コンピュータは自分自身が正しいことを証明できない。
証明しようとすると、必ず自己矛盾か無限ループに落ちるから
考えないようにしている。自己のことを考察した瞬間に
システムのどこかに必ず不動点が生じて、そこで引っかかって
抜けて来れなくなるのだ。

仲々良い所を付いているじゃないか
これはコンピューターばかりでなく人間にも当てはまる。

>>274 キングに証明させるのがよかろう。
奴は数学の召喚獣スクリプトだから。　普通あんなけレス出来んぞ。
キング無理すんなよー　オーバーヒートするぞぉー

talk:>>275 私を呼んだか？

>>276 呼んだよ？　数学が正しい事を自動で証明して見よ だって。

◆6fN.Sojv5w
等というking見た事無し

talk:>>277 では数学とはどのような命題か？
talk:>>278 何だよ？

>>279 中川さんに聞け。

このスレもう終わりか？

193

どうせ哲厨のスレだから終わりにして良い

521

どうせなら形式化された証明のデータベースの話とかしたいな。

MIZAR!

定理の自動証明ってMathematicaとPrologで既に商品化されてるよな

620

912

977

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


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

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

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

648

174

968

自動証明の研究に、何の価値があるの？

>>297
なぜ出来ないか考えるきっかけになる。

こらっつぐらいからやれば何がネックかわかるよ。

こらっつって３ｘ＋１と．５ｘをコンフォーマルマップで２つの
円のあいだの領域に飛ばして、グラフが１に収束する力学系を
つくればいいんでしょ？

>299

ありがとうです

f(z)=arg(z-p0)e^2π(1/(1+1/|z-p0|))i
は直線を同心円にマッピングする。

f(z)=arg(z-p0)e^2π(1-1/(1+|z-p0|))i
は直線を同心円にマッピングする。

こらっ

↓うるせーんだよ
↓このスレを見ている人はこんなスレも見ています。(ver 0.20)

610

それより証明を形式的に記述して検証する方法に興味がある

思考とは組合せ探索なり。

コンピュータで数万年かかるような組み合わせから
最適（に近いもの）を一瞬で見つけられるのはなぜなんだぜ？

きっと将棋のプロと同じ原理だよ

>>309
逆もあるよん

人間の場合超自然的な予見ができるから

人はそれを「当てずっぽう」と呼ぶ。

age

結局こういうことなんだよ
人間も全数探索に近いことをするけど、
コンピュータより早く終わらせられるのは、
その先に答えがあるかどうか評価する能力の違いなんだよ

ゲーム木を育てるジョウロだけじゃなくて、その枝を刈る鋏も重要なんだよ。
ようするに翠s

>>307
有名なんで紹介するのも気が引けるんだけど、Coqっていうソフトやら、証明
を形式的に記述して検証するものっていろいろあるよね。
その手のソフトの下地の理論を探れば、検証する方法の勉強はできそうだが。

>>316
プルーフチェッカのMizarってのをけっこういじったけど、
けっこう面白かった。

ただ言語仕様がどこにもはっきりと書いてなくて、(基本はpdfとかに書いてあった)
既存のライブラリを読んで自分で考えないといけなかった。

なんか基本は述語論理での推論法則だけを使ってやるって感じだったな
でも等式とかの導出を詳細に(両辺からxを引いたとか)書かないでも
成り立っててかつあんまり飛躍してなければ受理されたけど、
そのへんはどうなってるかわからなかった。

数学者は子供が覚えられる段階の算数→数学の段階から
論理的にすっきりした証明を選び出せば十分なんじゃないかなー
自動証明は証明可能かどうか、あと数学自体が無矛盾じゃないか、
の判定だけでいいと思う。

age

＞証明可能かどうか、数学自体の無矛盾の判定

ほとんどの数学理論では、無理。

つーか　例えば整数論なんて殆どパズルじゃん
heuristics を入れなきゃにっちもさっちもいかない
a! ha!なかんじは少なくともTuring Machineには無理だね

人間の脳を細胞レベル、分子レベル、素粒子レベル、、、で解明
できなければサル真似だよ

背理法ってなんかツンデレっぽくね？

べっ、べつにa=bなんて言ってないわよっ！
ただ、a≠bだったとしたら、
あれがあーなったりこれがこーなったりして
いろいろムジュンするって、それだけなんだからっ！

>>322
漏れは逆だと思う。

会うといつも笑顔で挨拶してはくれるが
二人きりで会おうとするとなぜかはぐらかされる。
だからあの笑顔は好意の証ではない。

>>322
お年をめした准教授が
「ツンデレって、なんやねん？」

ツンドラ気候か？って…

>>324
アニヲタには理解は早いかもしれないが
（アニメを知らない）准教授に説明するには
かえって困難だ

准教授の使っているパソコン（win95)みたいな性格のことですよ
と言っとけ

うちの弟は、平野綾＝ラムちゃん、だと思ってた。
それは平野文で「ふみ」と読むんだが。
（実はついさっき知ったｗ）

どうでもいいが
ガッキー＝ハルヒ　キョン＝マツケン
で「憂鬱」実写映画化って、あれマジで無いのか。

長門＝ホマキ　古泉＝平岡祐太　あたりまで
俺の中ではキャスティングが出来上がってるんだが
みくるが・・・・

>>322以降から
そろそろスレ違いっぽくなってきたな…

お前らアニメ板で語ってくれい

>>327あたりからアニヲタじゃなく
アイドルヲタのニヨイもしてきたが

ツンデレ教会は実在する

コンピュータによる将棋やチェスなどの知見を、定理の自動証明に
も適用できるのではないだろうか。過去の証明を沢山放り込んで
パターンを学習させることで、未知の命題が試行錯誤により、より良く
解けたりしないかな。
　特に、正しい命題の場合には、いってみれば詰め将棋のようなものだから、
どうだか分からない命題よりは易しいのではないだろうか？

4色問題みたいに扱われるだけのような

すべての組み合わせで成り立つ（あるいは成り立たない）ことを証明する場合と、
組み合わせの中からひとつでも成り立つ（成り立たない）ものを見つければよい場合は違うんじゃないかな。

>特に、正しい命題の場合には、

正しいかどうかが、そもそもわからないから、
そこで「正しいかどうかの判定」で、苦労するのでは？
「正しい（＝証明可能）」なことがわかっているのであれば、
そもそも機械で証明図を探索する目的が半減すると思う。

正しいとまず仮定して正しい命題用の思考を計算させる
そして偶然にも「正しい命題の場合」だったら、有用なわけだろ

実は俺、そーゆープログラム作ろうかと思ってるんだよな。
準ウィキ方式で、わりと誰でも参加できるからデータ量けっこう楽に増えると思うし。
たとえばAはa1,a2,a3...といった性質を持ってて、Aであり、さらにbの性質を持つとBであるとか、まぁ完全な証明ができるわけじゃないけど道筋をたたき出す感じで。
A→Zを証明するとしたら、Aのa3の性質はZであるための絶対条件であるゆえにZとかを自動で叩き出す。
証明って今までに出された結果が効率的に使えてないから難しいと思うんだよね。だったらそこはコンピュータにやらせようと。

絶対条件てなんだよ

ゴメス十分条件

>>331 データマインニング？

>>336
ちょっと興味あるんだけど、その「性質」ってどういうデータ構造？

>>336

おもしろそうですね。なるほど、自動証明って、
こういうことを研究するのですか。。

>331
おれは将棋のプログラム作ったことあるよ。
　弱いけどね。。。

　結局のところ、探索をどこで打ち切るか？というのは速度の
　問題でもあるが、つきつめれば盤面評価関数を
　どのように作るかの問題なんだ。

　盤面評価関数は、その盤面上の状況に数値を
　あてはめて、得点をつけるわけだ。
　それで得点の高いほうを選択するわけ。

　数学の証明をそのように得点化して評価できるかというと、
　多分、無理じゃないかな？

>>342

なるほど。
数学の証明に適用するには、
まだまだハードルが高いんですね。

数学の証明図の探索の場合は、
探索を途中て打ち切って得られた「証明図」が、
所要の命題に正しい証明を与えているか否かの判定も、
別に必要になりますね。

ゲーデルの不完全性定理により、そもそも不可能では？

>>336 が言ってるのは、証明探索とは別のアプローチかな？
証明を探索すると結果が出れば必ず正しいけど、なかなか現実的な時間では終わらない。
そこで結果の正しさをある程度犠牲にして計算量を削減しようと。

つまり、理想としては、「正しい場合」には、
正しい証明図がでるまで探索を続けるのだけれど、
現実問題として、探索を途中で打ち切らなければならない。
そのとき得られた解を、
今度は正しい証明図を与えているかどうかの判定にかける
（ミザールみたいなコンピュータ・プログラムで）
・・・ということかな？

証明図の探索はやらずに、もうちょっと粗い評価をするのかな、と思った。

先ずその定理が正しいことを証明すべきでは？正しいことがわかれば後はその具体的証明は稚戯に類すべきでは？高木先生の近世数学史談の正十七形の意見を参照。

３４９追加　然るに、ゲーデルの不完全性定理によれば、すべて命題の正否をコンピュータ式に自動的に決定することは出来ない。

10 for i=1 to ∞
20 if theorem=true print"QED"
30 next i

ループ変数使われてねええ

>>351
昭和のかほりがした

BASICだったらthenが要るし

そこは goto で無限ループだろ

ゲンツェンシステム

証明の検証だけでも十分便利だと思うけどね

二年。

747

>>357
実用化すれば、レフリー要らなくなるよね

コンピュータで検証できたらいいなと思うことはあるけど、
チェッカに渡す証明を書く手間考えるとやる気にならない

コンピュータでできる事はせいぜいMathematicaでできている事ぐらいじゃないかと思うのは発想が貧困ですか

>>361
お前さんは
メールを打つのが、手間かかるので
そのまま、電話をするタイプ？

>>363
いや、電話はなんとなく嫌いなのでメールする

>>362
貧乳だな

　　　　　　　　ｒ､　　　　　 　 _ .. ＞: : :ｿ`ｰ― ､}ﾉ　　　　　　　　　　 　 ＿
　　 　 　 _x≦メ_,-､　　 ,ｨ≦:_:.／:/ ;ｲi: : :j : : : :＼　　 　 　 　 　 {ヽ.__>､_ゝ
.　 　 　 ﾍﾆ　,ｨ r＜ 　 　 　 ／:/:/:/ {:| : ∧ : ヽヽﾊ　　　 r―-､ ﾉ-ｧ.勹
　　　　 ／ィヽ| ﾄ'ノ　　　　/ /.:| :{/＼ﾄ: :｣／Vﾊ:', } }　　　　,ｱ / 　 ｢`こﾍ
　　 　 　 　 ｀7_} 　 　 　 /,イ: :| ﾊｚ== ヽ{ =弍 | |:| |　　 ＜_へ＞　{　ｆ=} }_
　　　 　　,-､_fﾍxー､　　 　 |: ∧ {　　ｰ'ｰ'　 ･}:jﾊ{:.′ 　 __ﾍﾆｱ‐vｨｱﾄ､ヽ-'
.　　　 　 {／ヽﾉｲ¨ｰ'　　 　 �Y/: i＞ ､ 　　 _, ﾘ}│{　　 ﾍーｧ f ¨くtfｲ |
　　　　　 　ｨ_／　　　 　 　　　|: :|/:.,ｨ=厂{≧': /:∨　　 　 /／　 r=} ﾄ {__,ﾄ､
　　　　　 ／}fﾆニﾍ　　　　　　|: :|ﾍ　{¨7´ /: /＼:{　　　　　{ﾍ 　 ＜八_＿ ﾉ
　　　　≦ｨくﾄrｆ}f,勹　　　　　rﾍ: |∧ |/, イ :/　　⌒}　　　　|_.} 　 f{ ｨ=士ゝ
.　　 　 　 |_}ﾍ-'¨ｰ' 　 　　　人.ヽ{⌒{7＞.�W∧　/¨＞ 、ノ＾ﾆ勹　ヾ (f_ﾉｰ､
　　　　　 ／}ｰ士=　　　　 .ヘ `∧, 小、__} / : ｰｧ' 　,ノ 　 フ／ 　 　 　 ´¨
　　　　≦ｨく }`{z}　　　　　＼ Ｙ_./ /　{　　∨:/´ ｨ く　　ｰｆﾆ勹
.　　 　 　 |_}くニニﾍ　　　　/ ヽ/∨}／｢￣{ｱ:ー' : : ﾍ 　 ／,＜...
　　　　 r-ﾉ7_ __{ヾ> 　 ｰ≦.ｨ７/ /│　V ﾊﾍ : : : : : : ',≦ｆL ___fヾ>
　　　　 ﾌ / ,ｲｰ'¨　　　　 く/// /　:| 　 ∨ﾊ ',: : : ｊ: : :ﾊ ｧ/ ｲｰ'¨´
　 　 　 {./　ゞこﾌ 　 　 　 /// / 　 |　　 ∨ﾊﾊ: : :}Ｖ:}: |ﾑ{ ゞこﾌ
　　　　　　　　　 　 　 　 //7={...__　|　__ ...},ｘ≦: :ﾉ |ﾉ�X

ねぇ、誰も言及してないっぽいから言っとくけど、チューリングマシンって乱数とか無いぢゃん？
個人的には量子論的な乱数の存在がゲーデルさん的な「人間はコンピュータよりつおい」の根源的原因かもと思うのさ。
でさ、時刻とかカーソルの動きとか様々な外部要因を取込んで強化したぎじ乱数を、ぎじでもいいから使うべきだと思う。
既に与えてある定理の一部の文字をランダムに取換とか改変し、その文が論理的に正しい文になるまで取換や改変、を続けさせるとか。
与えられた語彙の中からランダムに定義行為や公理設定行為を行わせてみるとか。

論理的に通じるかは毎回チェックさせてさ。i^2=-1、とかで実数から虚数へ拡張とか結構平気でやりそうな気がするさ。
膨大な汚い小定理や汚い定義の中から、他の小定理や定義からの引用回数が多い程優先度を上げて処理し、
つまり母定理母定義、ハブ定理ハブ定義として進化論的に自然淘汰させるとか。googleみたいな。そこで「ネットワーク理論」とか応用してみたり。
つまり、貧乳は本人が気にしているのも含めて良いのやから誇られたらぐんにょりやね、に一票。

そんな擬似乱数で何かが変わるわけが無いがな

でもさ、ランダムにコピーミスしながら自己増殖するデータとかで「人工生命」という概念を確立した人もいるみたいだよ。計算力で膨大な世代を作れる上、寄生生物とか実際の生命の現象に似た現象が起きたりして色々面白いらしい。
人間が定理や定義の「善」をコンピュータにいちいち正すのは面倒。
というワケで〜進化論的に目指させればそれなりにそこそこの結果でるんじゃないカナ〜と思う。なるべく簡潔で汎用性の高いのが生き残ってゆくとかさ。
人間の理性的処理能力だってもともとは遺伝子のコピーミスというぎじ乱数から出たっぽいしさ。

何をやりたいのかよく判らない．
自動証明したいの？数学の定理生成をしたいの？
新たな数学体系の構築をしたいの？

>>106
ヒント【ゲーデルの不完全性定理】

>>372
不完全性定理がどうしたって？

>>370
その方針だと計算の効率とかには影響を与えるだろうから、
効率のいい（擬似）自動証明方法とかは思いついてくれるかもしれないが、
>>367で書いてるゲーデル的な意味での性能は一つも変わらない。

というか、ちゃんと勉強すれば簡単に分かることなんだけど、
例に挙げているような擬似乱数の類では
コンピュータの計算可能性そのものに関しては何も影響を及ぼさないぞ。
せいぜい計算量レベルの影響しかない。

838

425

目的別で選ぶ定理証明器

1. 俺が書いた証明をチェックしたい　→　Proof Checker　(Mizar)
2. 定理をあたえたら全自動で証明を返してほしい　→　Automatical Theorem Prover　(Djinn, Mathematica)
3. 半自動で証明を手伝ってほしい　→　Proof Assistant　(Coq, Isabell)

ただし、2.は扱える領域が極めて狭いので注意!! そして、証明できないときもある。
1.3.はすべての数学的命題を扱うことができるが、人間の努力も必要である。

age

>>377
2は、証明できない場合、フリーズしちゃうんですか？

>>379
証明器によると思う。よく知らない。
ただ、計算量は指数的に膨れ上がる事が知られており、自動証明可能なものであっても、
現実的な時間内には終わらないこともある。
そもそも、自動証明では記述できる命題が限られるため、証明支援器 (377の3.)を用いて、
部分的に自動化する方法が最も現実的である。

>>380
ありがとう。

(ﾟДﾟ)≡ﾟдﾟ)、ｶｧｰ ﾍﾟｯ!!

(ﾟДﾟ)≡ﾟдﾟ)、ｶｧｰ ﾍﾟｯ!!

ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに

(ﾟДﾟ)≡ﾟдﾟ)、ｶｧｰ ﾍﾟｯ!!

ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに





ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに

ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに





ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに

ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに





ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに

ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに





ん？タン虫は２連で終わり？
つまらん！

１０００までやりゃいいのに

１０００までやんねぇのかYO？
いくじなし＾＾









１０００までやんねぇのかYO？
いくじなし＾＾

ん？もう終わりｗ

>>320
> ＞証明可能かどうか、数学自体の無矛盾の判定
> ほとんどの数学理論では、無理。

無矛盾性の証明が無理なのでは無く、無矛盾な公理系の上での
すべての真な命題の証明が無理なのでは。

僕は以前は形式的体系ということについて、色々思うことが
有ったのだが、この頃は、Frege構造というものについて気に
なってきたのだよ。フレーゲ構造って、なんか面白そうな予感
がする。

>>393
フレーゲってよく知らないけど、普通のhigher order logicと何が違うの？

AgdaとかCoqとかを勉強したいです。でも全然わからないです。おすすめの初心者向けの文献はありますか？

Lectures on the CurryHoward isomorphism
ttp://citeseer.ist.psu.edu/519604.html

未来言語Agda
ttp://d.hatena.ne.jp/yoriyuki/20080627

age

最近集合論を形式化したノート作ったんだけど、せっかくだからプルーフチェッカーにでも通して遊んで
みたいんだけど、個人的に遊べるソフトはどれがお勧めですか？

今、MIZARとか言うのを解読中なんですが、HIDDEN.VOCが見当たらないんだよねえ。関数記号とかも
自分で定義したいんだけど、そういうのはＭＩＺＡＲには向いてないのかなあ。

もっとグラフィカルでわかりやすいのがあるといいなあ。

もしかして>>377ですべてなのかな。そうだったらごめん。

>>399グラフィカルってのは現状むずかしいんじゃないかなぁ。
それより、そのノートを公開すれば、いろんな人が各ツールで実装してくれんじゃね？
それをグラフィカルに眺めればok

age

「全ての命題を自動証明することは出来ない」は必ずしも
「ほとんど全ての命題を自動証明することは出来ない」を意味しない。
もしかすると、
「ごく一部の命題（測度０笑）を自動証明することは出来ない」なのかも
しれない。
また、「正しいと証明できる命題であっても自動証明することは出来ない」
を意味しないことに注意。

ある一つのパターンの命題（証明不能の証明に出てきたようなタイプの
命題）だけが、証明不可能であるだけなのかもしれないのだ。

くだらん妄想膨らます暇あったら本読めよ。

初等幾何に限定すれば定理の自動証明はある程度上手くいったりしないかな
補助線引いていくだけだったりするし

>>405

無理でしょうな。平面幾何の定理は非常に多くあるし、その証明は難しい。
よって機械的に証明を探索しても計算量が爆発してオワリ。

よくＴＶか雑誌などに、詰将棋３〜５手詰なんかあるじゃん
あれって、過去に出された（既出）な問題ってのもあるのかな？ってふと思った

とあるマニアな人間が、過去（１世紀以上も）の詰将棋問題を
データーベースみたいなものに、インプットしてて
例えば今週出題された、詰将棋問題を、そのデーターベースで"検索"したら
ヒットして、19xx年xx月xx日 読＠新聞 にて、同問題がありました　とかね

ｳﾝ十年前のNHKで、将棋の特番だったかうろ覚えだが
詰将棋などではなく、実際の戦いの局面の配置を、コンピュータでインプットして"検索"し
同局面が、過去に3度ありました。と出て、先手後手どちらがその後有利または勝ち負けなのかなどの
判定らしきものが、あった。

ウン十年前はさすがにないでしょ

たぶん数年前の順位戦A級最終日の中継で勝又5段（当時）がデータベース使ってたときの事だと思うけど

>>408
ウン十年前ではなくて、十ｳﾝ年前か
羽生さんが、全盛期の頃
（今でも、健在ですが・・・）

これと似たようなもんでさ
高校教諭が相加相乗平均に新証明法
http://www.asahi.com/science/update/0816/OSK200808160004.html

この相加相乗平均の証明方法は５０以上あると
それらをデーターベース化して、証明の"判定"みたいなものを作れないかな？

　「この証明方法に気づいた人はこれまでにもいたはず。
簡単すぎるので発表済みと思ったのかもしれない」

既出な証明であった or 新証明である とかね
そしてこのような判定プログラムを一般人の人でも、扱えるシステムを設けるとかね

YASUHARU UCHIDA (Kurashiki Kojyoike High School)
A SIMPLE PROOF OF THE GEOMETRIC-ARITHMETIC MEAN INEQUALITY

http://www.emis.ams.org/journals/JIPAM/images/080_08_JIPAM/080_08_www.pdf

三年。

>407
遅レスですが「詰め将棋データベース」はもちろん存在します。
但し、有償でかなり高価なものらしく（セット全体で10万円くらい？）
Web上などで誰もが検索や同不同チェックができるようにはなっていないようです。

>>412
参考になりました。ありがとうございます。

詰め将棋データベースの同局面検索機能みたいな感じで
それを数学に使えないかなってね。

例えば、大学入試問題。
大学側が、いろいろ問題を考えて作る。
しかし過去にどこかの大学で似たような問題（または、全く同じ問題）があったらマズイよね

そのような検索機能があったら便利かなってね。
実際は、人間たち（教授・准教授その他）が、案外手作業で探っているのかもしれないｗ
過去問題集（赤本）とか引っ張り出してね。

事実、国語の分野では、煮詰まっているらしく
過去の問題を使いまわしを認めるかどうか検討しているらしい
（それは、著作権などの問題があるので、円滑には進まないとか）

age

コンピュータでトレミーの定理の自動証明に成功した

凶悪的に強いチェスソフトを教えてくれさい

>>415
アルゴリズムうｐ

Mizarって言う定理証明支援システムがあるの知ってる？
その言語で数学の論文書くと証明をチェックしてくれるんだってさ。
いまそれでチェック済みの論文がデータベース化されていて、
そこで既に証明済みの定理も新しい定理の証明に使用できてそれをまたチェックできるんだって。

ttp://www.cs.ru.nl/~freek/mizar/

ただしその言語での論文は通常の4倍くらいの長さになるそうな。

>>418
Mizar自体は激概ではあるが、しかし僅か4倍で済むというのは意外だった。

Mizarで書いた論文は普通の雑誌だと受理されるのかなと思ったが
労力的に絶対無理だから考えるだけ無駄か

つーかMizarって、どんな言語を使っているの？

age

コンピュータは０と１、すなわち真か偽かの二種類。
数学はゲーデルの不完全性定理により真でも偽でもない命題がある。
だからコンピュータと数学は合わない。
真でも偽でもない命題をコンピュータにやらせたら
無限ループに陥る。
その場合は
if p<>true and p<>false then
exit sub
endif
と書くといい。

わかってねえな

わかってないな

取り得る可能性が有限の場合はコンピューターはすべての可能性を実行して反例を探せばいい
すべてのパターンを実行しても反例が見つからなければ証明されたと言える

無限の場合は無理

むかし第五世代というインチキなのがあったけど？

クラウドコンピューテイングでゲーデル数解析マシンをつくればすべての定理は証明されてしまう。

ttp://www.too.com/dtp/proofcheckerpro/
紛らわしい名前のソフトがあった

800

>>428
そんなわけねーだろ

そういえば数学板には数値解析のスレがないね
どっちかといえばシュミレーション板やプログラム板になるのかな
でも理論的なことを語るのに数学板にも一つぐらいあってもいいと思うんだが

>>432
シュミレーション？？？

大丈夫ですか？

数学板、誤変換（旧）

○確率
×確立

○置換
×痴漢

○偏微分
×変微分

○整式
×正式

○小数
×少数

○有理化
×有利化

○対数
×大数
（ただし『大学への数学』または"大数の法則"の意の場合も・・・）

○シミュレーション
×シュミレーション
（日本語にない発音のため。ただし方言には近い発音があるらしい）

○キチ（既知）
×ガイチ
（またちなみに、既出（きしゅつ）と読む。"がいしゅつ"ではない。）

○可算無限
×加算無限

○最大元
×最大限

○単項イデアル整域
×炭鉱胃である聖域

>>435
一番下ねえよｗｗｗｗｗｗｗ

>>435 wwww あるある

o 正則行列
x 生息行列

o 単射である
x 単車である

o 閉包を得る
x 兵法を得る

>>1
無理だろ。
そもそもC言語もVBもmathematicaも、√2の計算すら
どうせどっかで四捨五入してるんだろ？
じゃないと永久に表示できないからな。
定理の証明に四捨五入なんてしたことないぞ、おれは。

>>438
なんでコンピュータがわざわざ四捨五入とかいう十進法に依存した方法を使わなならんのだ

２進法なら、零捨一入かな

>>438
大して知らないのに、知ったかすると恥ずかしいよ。

>>441
なら答えてもらおうか。
√2の計算は四捨五入するかしないか。
定理の証明において四捨五入するかしないか。

物理じゃあるまいしなんで証明に無理数の計算が必要なのかと

PrologのスレにFORTRANが来たって感じだな

√2の計算がどうとか言ってるやつは高校数学程度までしか知らないの？

√2は単に x^2-2=0 の根であるということを意味する記号として扱える。
実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、
証明に使う性質は、「x^2-2=0 の根である」という代数的性質から全て導かれる。

まあ、実際、代数学の証明の幾つかは既にコンピュータに載せられているものもあるし
人間が既にやった数学的証明は、コンピュータに載せることは可能。

ただし、コンピュータが人間の解いてない数学の定理を証明するような
自動証明ができるかどうかとなると話は別だが。

>√2は単に x^2-2=0 の根であるということを意味する記号として扱える。
>実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、

例えばC言語は10桁目で四捨五入するようになっていると仮定する。
√ｘと√ｙは18桁目までは同じで、19桁目から違う数になるとする。
するとC言語では√ｘ＝＝√ｙとなってしまう。
√○を記号として扱おうがこれは避けることの出来ないものだ。
するとC言語では実数の大小関係が確定できないことになる。
大小関係が確定できないということは、実数における命題のほとんど全ては
証明することができないことになる。

あ〜、こうか。
if(x=!y)
{
while(√ｘ＝＝√ｙ）
{
√ｘの小数点以下を求める処理
√ｙの小数点以下を求める処理
}
}

というわけで>>447は取消ということで。
しかし、コンピューターで証明というのは無理だと思うね。おれは。

>>447
計算機での証明を行う場合も、四捨五入なんかする必要はない
>>446のように何らかの代数的性質を満たす記号として √ を導入すればいいだけ

√x と √y の大小関係もその代数的性質から証明できる話。
>>448のやり方がそのひとつだな

まあ、コンピュータによる完全な自動証明は無理だが、
人間がやる証明の支援くらいは出来るようになるかもしれないとは思っている

あ、思ってるというか、このスレで何度も出ているように、
一応コンピュータでの証明支援は既にあることはある。

数学の知識そのものがお粗末なんじゃないの？>>447は。

マテカを使った事は無いとみた

ver3から使ってるよ。
ver4から3次元曲面がマウスでぐりぐりできるようになったよね。

あれば実数を小数有限桁打ち切りで扱うなんて発想は普通出てこない

じゃあなにか。

あらゆる実数に関する命題は
具体的数値（1,2,3,4,5,6,7,8,9,0）を全く使用せず
抽象的数値（a,b,cなど）で全て証明することができる。

という定理があるということか？

少しは数学勉強せーーよ。おめーみてーなやつに長々と説明なんかしたくねーーんだよ。

とりあえずTrace関数でMathematicaがどういう厳密値計算をやってるか追ってみるといい

ゲーデル数のようなものを導入すれば可能かもしれないと思ってる。

>>456
長々と説明なんてしなくていい
そういう定理が「ある」か「ない」か
2文字で済む話じゃないか。

だって問いが意味不明なんだもの
√2を小数で表した物が具体的数値で√2が抽象的数値だって？
誰の脳内設定だよ　実数の構成も理解して無いだろ

>>438は√2の計算をどっかで四捨五入せずにできるのかｗ　凄過ぎるｗｗｗｗｗ

質問自体がトンチンカンなんだよなあ。第一
＞そういう定理が「ある」か「ない」か
に答えてもらえば解決すると思ってんだからなあ。マナカナのどっちが美人かを決めれば
解決すると思い込むのと変わらんよなあ。

結局、バカは自分がバカだと認識することはできないんだなあ。

>>461
晒しあげ

>>455は「実数」に「あらゆる」という語をひっつけることの恐ろしさを知らない

>>462
そんな長い文章はいらない。2文字でいい。
>>464
実数に関する証明はあらゆるをつけなければ意味がない。
たった２，３個の実数で成り立った所で何の意味もない。
∀a∈Rについて成り立たなければそれは実数における定理の資格はない。

抽象的な文字（a,b,c・・・）で解決できるから
具体的な数値など求める必要はないと言ったのはそっちだ。
そういう定理がなければそんな発言は出てくるはずがないからな。

>>463
どっちが晒しあげられてるかも気付かないのね・・・

そんなに答えだけが欲しいんなら答えてやるよ
「ない」
というか具体的数値とやらを使用しようがしまいが
あらゆる実数に関する命題を全て証明することはできない

>>466
晒しあげ

あげ忘れたｗ

釣りじゃないんだよね？
Mathematicaで「√3＞√2」を評価したとき
それぞれを小数展開してそれらの各桁を比べてるとでもと思ってるの？

ならおれの勝ちということで。
ではでは。

おめ

>>455の
＞あらゆる実数に関する命題は
は
あらゆる実数に関する「証明済みの」命題は
ってことね。

ん？　どうした？　満足したんじゃ無かったのか？
本当に知りたいなら付き合う気はあるけど
言葉遊びがしたいだけなら流石にやる気は無いぞ

自動翻訳があの程度のレベルなのに数学の定理の自動証明なんて出来るわけない

自然言語と違って厳密だからね
超数学的なことをせずスピードを問わないのならどうとでもなる

形式化する段階がかなりウザイだろうな

おれは言葉遊びなんてしてない。
真実追求しかしていない。
抽象的数値a,bには大小関係が定義されていない。
aとbどっちが大きいか？という問いに意味がない。
アルファベットに大きいも小さいもないからな。
a、bに具体的数値を代入して初めて大小関係が定まる。
ところが、ここの住人は具体的数値を求める必要はないと言う。
じゃあ質問するがaとbはどっちが大きい？
ただしaとbには具体的数値は代入されていないものとする。

ただ、おれは>>448で大小関係はプログラムで求められることに気づき
その部分においてのみ、自らのあやまちは認めたはずだ。

>>478
晒しあげ

＞ところが、ここの住人は具体的数値を求める必要はないと言う。
どのレスだよ

　

x,yを、x＜yなる実数とする。
a^2=xを満たす正の実数aと、b^2=yを満たす正の実数bがともに存在するとしよう。
このとき、a≧bと仮定すると、x=a^2≧b^2=yとなり矛盾する。
従ってそのようなa,bが存在すれば、a＜bである。

バカはほっとこうよ。つまんね。

＞x,yを、x＜yなる実数とする。

この時点でダメだな。
単なる文字に大小関係は無いの。
ｘ＜ｙとする
なんてやってるということはｘとｙにはなんらかの実数、
つまり具体的数値が代入されていることを予定しているんだろ？
アルファベットに大小関係は無いの。
もうほっとこう。だめだ。

>>484
（´,_ゝ｀）ﾌﾟｯ

無限小数表現のことを「具体的数値」とか言ってる中学脳が
吠えてるスレはここですか？

>>484
晒しあげ

これってさ、コンピュータに何かを発明させるってのと同じくない？
内燃機関を発明できるか？
どういう構造にしたら効率がよいか、とかは得意だろうけど

仮にできたとして、
内燃機関を発明するアルゴリズムは、内燃機関を知っている何かでなければ構築できないのではないか？

プログラムというのは
実際に打つ前にフローチャート書く。
（フローチャートを書かなくても、図とか絵とか描いて矢印書いたりして
なんらかのフローチャートもどきは書く）
ならそのフローチャートが証明になっちゃってるじゃん。

>>489
自動証明ってのは、プログラムを生成するプログラムを書くような
ものなんだよ。

>>490
そのプログラムはフローチャートでは表すことは出来ないの？

証明可能な定理に関しては、その証明を見つけ出すアルゴリズムがあるっての
知ってていってんだろうな。

つーか。ゲーデル数化も何もしらなそうだな。

次の複素数と共役な複素数を言え。「2-8ｉ」
↑教えてください！

素朴な質問なんだけどそういうのもアルゴリズムって言うの？
アルゴリズムって言うとき、自分の感覚では、証明出来るなら証明し、出来ないなら出来ないと有限ステップでわかるようなものってイメージなんだけど。

>>493
マルチ

何の定理でもいいんで
その定理が真であることを求めるプログラムをCでも何でもいいんで
書いてもらえませんか？
ピタゴラスの定理でもいいですよ。

>>494
いやいや、すまんかった。結局こういうやつ>>496がいるからさあ。ちったあ入門くらい自分でやれ
と言いたくなる。

>>496
少しはヒント出すか。１，２，３，．．．と自然数を順に調べていけば、その中にピタゴラスの定理の証明が
あるんだけど。意味わかんねーだろ。だから、ゲーデル数化ぐらい知っとけっての。

あ、それから、真であることを求めるプログラムじゃなくて、証明を見つけるプログラムな。
真と証明可能の違いくらいも早く知っとけ。

>>498
うん、わかんね。
真と証明可能の違いはわかる。
真だからといって証明可能かどうかは保障されてないもんな。
でも証明可能なら真ってことだ。

ちなみにピタゴラスの定理だとCで何行ぐらいになるの？
だいたいでいいんだけどさ。
500行ぐらい？
それとも100億行ぐらい？

証明を見つけるプログラムってprintfで表示するの？
日本語で？

計算機での自動証明の話で、
ヒルベルトのプログラムだのゲーテル数だのを持ち出す方が
よっぽどバカだと思うのだが．．．。
そういう無茶な風呂敷の広げ方をするから、
一般人は>>500のような反応をするわけで。

実際に自動証明の研究でやっていることはといえば、特定の分野で
限られた定理の組合せで証明できる範囲に限定して、
前提となる事実・帰結・推論規則としての定理・定理を適用する上でのノウハウ
等を、その範囲に限定して設計された記述言語で記述しておいて、
それらを利用して、人間には比較的簡単に行えるような証明を構築するプロセスを
計算機にトレースさせるというような試み。
つまり、人間にできないような証明を計算機にやらせるなんてことを
いきなり目指してるのではなく、まずは人間の思考というものを
プログラムでモデル化してみることで、人間的な有機的な物事の捉え方を
計算機で応用するための知見が得られないかを探る基礎的な研究であって
本質的には人間工学に近い分野。あとはノレッジベースとかＡＩ（死語）とか。

実際に素材としている数学の分野は、簡単な定理の組合せで証明できる
初等幾何が主流。それも、ピタゴラスの定理のように数値の計算が
からむようなものは「簡単な定理」の範囲に入らない。

証明可能な命題の集合と有限ステップで証明可能な命題の集合が異なる以上
ゲーテル持ち出しても何の意味もない

>>503
有限ステップでは証明できないが、証明可能な命題ってあるの？

ω規則があるならあるでしょうな

>>502
をを！すまんかった。今は反省している。どうも>>498を読んだときバカにされた気が
して感情的になってしまったようだ。

おわびに、ゲーデル数化をしても、定理の自動証明にはあまり実用的でないということ
を例えで説明しよう。まず、使用する文字を決める。例えば、ひらがな全てでも良い。
カタカナを含めてもよい。いずれにしても使う文字は有限個に決める。例えばN個だと
しよう。文字を2つだけ並べた文字列は有限個しかない。今の例ならN×N個だ。文字を
3つだけ並べた文字列も有限個。4つ並べても有限個。．．．と行くと、いずれは例えば

ふるいけやかわずとびこむみずのおと

というような文字列も現れるし、ピタゴラスの定理の証明として読める文章も現れる。
それに、以上の手続きは簡単なアルゴリズムで書ける。もっと詳しく論理式とか、証明
を定義すれば、任意の文字列に対して、それが何らかの定理の証明になっているかを
判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
あるかどうかの判定をするアルゴリズムも書ける。

（すまん。上の>>498は>>489のまちがい。）

だからといって、以上の方法が実用的でないということは容易にわかると思う。現在の
コンピューターでは演算速度も記憶容量も足りなすぎる。もちろんいずれ以上のような
方法でも十分実用になるような性能を持ったコンピューターが現れる日が来るかもしれ
ないが、そのころにはの方法で、もっと効率よく定理を証明するアルゴリズムが開発さ
れているかもしれない。

長文すまんかった。失礼。

あ、実用的でないというのは「たとえ証明可能であることがわかっている命題の証明を探すとしても」
実用的でないということ。

>ピタゴラスの定理の証明として読める文章も現れる。

なるほど。その発想はなかったわ。
行間を読む行為もしなくて済むだろうし。
要するに定理の証明とは「有限個の文字の羅列」なんだね。
でも、ここで数学をかじってる人間はすぐに一般化したくなると思うんだ。
「無限個の文字の羅列」で表される定理の証明はあるんだろうかとか
「文字と文字の間にじつはさらに文字があるみたいな、実数の稠密性みたいな文字集合」とか。

ところで
数学の定理は有限個の文字で証明できる
という定理はあるの？

真偽を証明できない命題がある以上そんな定理はないだろ

数学基礎論でいう定理の自動証明ってのは>>498が言うようなものじゃないんだが

スレタイと１の延長で話してるなら、基礎論が出てくること自体おかしいってことだろ

有限個の文字の羅列でも
文字数が確定していないんだから
文章の数は無限個だから証明の文章はできないんじゃないの？
ある定理は100文字で証明終わりになるとはじめからわかっているなら
100個の文字のあらゆる組み合わせを調べつくせば済むけど
その定理の証明が100文字で終わることをどうやって事前に知るの？

基礎論の一分野として自動証明をしてる人もいるから
>>498が話してるような方面の基礎論は関係なしで

あ.あ
あ.いうえおか
か.なにぬね

こういう文字集合を定義したら
証明できる命題は増えるんでしょうか？

>>505
ω規則ってどんなのですか？

わかってないなぁ。

科学が信仰する事実そのものという観念は、宗教、特にキリスト教の神観念に近い。
これは科学が西洋社会を起源にもつ文化現象であるという一つの証拠である。
キリスト教の神観念は、人間の外にある絶対者であり、人間にとって認識不可能かつ到達不可能な存在である。
これは正しく科学が前提とする事実そのものの存在と同じである。
ちみなに、仏教では一切の存在に仏の生命が宿ると考える。
仏性=真理は外にある絶対のものではなく、個々の存在に宿る内面的なものである。
真理は自身のうちにあり、外にはないと考える。
科学は真理を人間の意識の外に求めようとする点において、極めてキリスト教的、西洋的である。
到達不可能な絶対者を立てる科学は、キリスト教と同型の思考形態をもつ。
真理そのものがはなから自己のうちに宿ると考える仏教的発想によって、科学は相対化されるのである。
また、構造構成主義もシステム論も、意識から隔絶した事実そのものを定立することなく、世界を記述するので、科学とは観察方法が根本的に異なることになる。　

誤爆か？

いいえ、スパです

おいおい、逃げるなよ。
文字に大小関係を導入したとたんに逃げるか。
おれだよ、おれ。
文字に連続性を持たせたとたんに口を閉ざすか。
もっとさらし上げろよ。

お前一人で何の話してるんだ

>使う文字は有限個に決める

だから使う文字を有限個にしたところで
出来上がる文章は無限個だろ。
そんなロジックもわからないのか。
あ
ああああ
ああああああああ
ああああああああああああああ
わかるよな？
あだけで無限個文章があるよな？
まさか逃げはしないよな？

だからどうした

そんなに十進表記が大好きでそれで上手くいくと思ってんならそれでやってけばいいよ
グッドスタインの定理を途中に出てくる式全部きっちり計算して証明すればいいし
チャイティンの定数も十進表記で計算し終わってから議論すればいい

おいおい、本当に逃げちまったよｗｗｗ

アホ過ぎワロタ

>>525
晒しあげ

>>527
よく戻ってきたな。
じゃあ話を聞かせてくれ。
ゆっくりでいいぞ。
緊張しなくていいんだぞ。

>>528
晒しあげ

　　　　　　　　　　　　　　　　　　　　　　　　　　 ＿,====ミミﾐヽ、
　　　　　　　　　　　　　　　　　　　　　　　　　,,==≡ミヽミヾミミミ、ヾ、
　　　　　　　　　　　　　　　　　　　　　　 _=≡≡三ミミﾐ ミﾐヾ、ソ)),,》　　.
　　　　　　　　　　　　　　　　　　　　　彡彡二二三≡ミ-_　ﾐﾐ|ノﾉj )||ヽ,　)、
　　　　　　　　　　　　　　　　 __,,,,,,,,,／彡二二二　　　 ,-　__ﾐ|/ﾉ ﾉﾉﾉﾉ)　||
　　　　　　　　　　　　　　　　-=二ミミミミ----==--'彡 ∠ミﾐ_ソノノノﾉ　ﾉ
　　　　　　　　　　　　　　　　　　/／＞=''"二二=-'"_／　　 ノ''''')λ彡／
　　　　　　　 ,,/￣''l　　　　　　 彡/-'''""￣-=彡彡／　,,-''",,,,,,,ノ .彡''"
　　　　　　　(,　 ,--(　　　　　　彡 ,,-- ===彡彡彡"_,-＿　　　ヽ　Υ
　　　　　　　ヾ-( r'''''＼　　　　／／=二二''''''彡ｿ￣ ∠__＼ .＼ｿ　 .|
　　　　　　　　　＼;;;;　 ＼　　　Ζ彡≡彡-'''',r-､>　　　l_"t。ﾐ＼ﾉ,,r-v　　　／￣￣￣￣￣￣
　　　　　　　　　　 ＼;;;;　 ＼　　彡""彡彡-//ヽ"　''''''""￣'''""(ｴｱ/　　／
　　　　　　　　　　　　＼;;　　＼'''''')彡ヽ//　|　(tv　　 ／|　　,　r_>'|　　＜一体みんな誰と戦っているんだ
　　　　　　　　　　　　　＼;;;　　＼'"　　＼　,,"''-,,ﾉ,r-", /　　r'''-,　.j　　　＼
　　　　　　　　　　　　　　 ＼;;;　　＼　／,,>--'''二"''' r-|　　 二'" /　　__　　＼＿＿＿＿＿＿
　　　　　　　　　　　　　　　　＼;;r'""彡_l:::::::::::::::::::::: /./_　　　" ／￣￣"===-,
　　　　　　　　　　　　　　　　　 )''／／rl_--::::::::::::::::/:/ヽ"'=--":

>任意の文字列に対して、それが何らかの定理の証明になっているかを
>判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
>あるかどうかの判定をするアルゴリズムも書ける。

ええ、うそでしょ？
ならそのアルゴリズムがすでに定理の証明になっちゃってるじゃん。

>>531 この>>506が言っている3行は事実。証明と定理がラムダ計算の式と型に対応しているという理論(Curry-Howard対応)
を使えば、ある文字列(式)がどのような定理(型)を証明しているか、それとも間違っている(型エラー)か自動判定することができる。

しかし、逆に、定理(型)からその証明(式)を導くことは完全自動では無理。

高校レベルの問題なら、自動的に解いてくれるプログラムが完成したよ！もちろん、定理の証明も可。

問題を入力すると、その問題を２ちゃんやYahoo!やOKWaveとかの質問スレに自動的に書き込んで、結果を読み込んで戻ってくる。
そういう掲示板だけでなく、あらかじめ指定したアドレスへ質問メールを出して、返答を受けることも可能。
これで殆ど解決。

でも最近、回答の精度が落ちてるんだよなあ。「マルチポストはヤメレ」「質問ばかりするな」なんていう意味のない回答が良く来るようになった。
どうしてこうなったんだろう。プログラムのミスかなあ。
この辺をどう解決するかが今後の課題。

>>532
虱潰せばできるけどね
簡単な定理でも地球が滅びるくらいの時間が掛かるだろうけど

talk:>>533
それは反則ではないのか？

Reply:>>533 その計画書を私に見せてみろ。

トースターによる定理の自動コピーとか

証明はDNAパソコンでしょ

>>533
そういうソフトはすでに存在しているんじゃね？
オープンにされてないだけで。
簡単につくれるし。

「九九」の歴史は古く、中国の春秋時代（紀元前七七〇年から紀元前四〇三年）にまで遡ります。春秋五覇の一番目、斉の桓公（B.C.685-643) が人材を求めた時に、「九九」 を暗記しているという特技で採用された者がいたという記事が残っています。

大学入試レヴェルの『数学的帰納法』を
プログラムによって解かせるものを考えた。

でもこれって既出かな？？？

マジで!
ソースきぼんぬ

どうせ再起呼出し使うだけなんじゃねーの

コンピューターの完全寿司ロボットをつくれば世界に売れる。
ネタの仕込みからにぎりまで

そばロボットもいい

確かに、簡単なものしか使っていないから既出だと思った。

『数学的帰納法』で
１．等式の証明
２．不等式の証明
があるけど

正の整数（自然数）のみ動かせば
負の整数の場合も自動的に掃きだしてくれる。

>>540 \forall n \in N, P(n).
の証明を
P(0) かつ \forall k \in N, (P(k) => P(k+1))
を使って自動証明するってことだよね。
具体的にどんなことが自動でできるの？kwsk

あたりまえだがすべてのnについて計算するわけじゃない
論理的に式変形をしてしらみつぶしに解いていくだけ

>>546 x + y = y + x
とかも自動証明できたりする？

>>547
ぜひどうなるか知りたいね。

>>547
∀x, ∀y, x + y = y + x が自動で証明できたら
かなりすごいんじゃね？

>>549
そんな単純な問題なら一瞬で証明できるわな

>>550
してくれ

>>550 してくれ

>>550
してくれ

>>550
して。

>>550
頼む

しらみつぶしってことはどうせ簡単な定理を証明するにも宇宙の寿命ぐらいの時間が掛かるんだろ？

dim x as string
dim y as string
dim + as string

でできるじゃん
あとは配列にいれてソートしてイコールになればＱＥＤ

定理の自動証明はＣＵＴ規則で空節が導出されりゃよい。

>>557
わからん kwsk

確かＰ算術とかいう簡単な演算体系の定理を証明するのに非決定性アルゴリズムで2重指数時間かかるという定理があったな。
定理の証明を実際的な時間で証明するのは何らかの支援が必要でしょうな。

コンピュータに出来る訳がないだろwwww

>>560
2重指数時間かぁ・・・
それは絶望的だな

2重指数時間でも自動で出きるのはすごいと思う。
>>549なんかはxとyの組み合わせが無限にあるから、有限時間には終わらない。

2つの関数が等しいか否かのチェックって決定不能問題だよな

将棋や自然言語処理のように、いっぺんコーパスの料理の仕方が分かれば劇的に進歩するだろうな。

>>549なんて幅優先探索でλ計算すればすぐに解けるじゃん

プログラムは可算個しかないのに、決定問題は非可算個存在する。
決定不能問題のほうがはるかに多い。

でも記述可能な決定問題は可算個しかないからねｗ

計算尺があるだろ！

誰にレスしてるんだ？

KLEENEの階層を数学者ががんばったのは計算不可能な領域が広大だと思ったからだろう。

計算尺で計算量を測るという発想はおもろいね。

「帰納的集合」だけに限っても計算量的にはかなりでかいクラス
EXPTIMEとかも余裕で含むので「現実的には計算不可能な」
証明がほとんどと見なして差し支えないかと。

しかし計算量では多項式時間かどうかが重要なようだが２乗もあれば追い付けなくないか？

計算時間に関してはO(n^2)のアルゴリズムは十分実行可能であることが多い。
世の中から単純ソートが無くならない所以。
数値解析や数理計画のように実行回数が少ないものはO(n^3)でも歓迎されるくらいだ。
空間計算量の方はもっと厳しくて、理論上指数時間のアルゴリズムでも、
実用上はメモリの制約の方が先にやってくるというのはよくある話。

定理の自動証明だと定理パターンの組み合わせの適用で解くから
しらみつぶしにやると当然指数的に増加していくな

ソフト開発の現場にいる連中はアルゴリズムの計算量を議論することってあるのかな。

>>575
うーん、やっぱり２とか３まで現実的か・・・
例えばＲＳＡが多項式時間で解けるようになったとして、何乗ぐらいから無意味になるの？

定理の証明をしらみつぶしって解析学では不可能だろ。
実数だから、0、0.1、0.001とかしらみつぶしにしても永久に１までたどり着けない。
離散数学なら4色問題とかでできるんじゃないかな。

>>577
？？？
処理のエンジン部分を開発しているチームは、日々それと格闘しているだろ。
ループの回し方１つで、処理時間のオーダーが変わる世界。

>>579
変数に代入する値をしらみつぶしとはだれも言ってないと思うが。

そもそもメモリーセルがON,OFFの離散だから
連続を扱えるはずがない。
お絵かきソフトで直線を書いてもドットの粒が並んでるだけだよ。
直線は絶対にかけないよ。
それどころか紙と鉛筆ですら直線は書けない。
鉛筆の分子が有限個、紙の上に並んでいるだけだから。
というかこの世は離散だから解析学は滅びるべきだよ。
実数も。

Reply:>>581 それでは現象を表現する方法を述べよ。

>>582
お前がやれカス

Reply:>>583 実数を使う。

>>頭の良い皆さん


ムカつく奴が計算自慢してます。どうか、皆さんでそいつをギャフン(死語ｗ)と言わせてくださ！

板は・スロットサロン
スレは・しのけん
ですm(__)m

ちなみに…∫[-∞,∞]cosbxdx/(x^2+a^2)の値を求めよ、は？

みたいなのを出して答えられないとバカにしまくり。どうか、よろしくお願い致します！m(__)m

Reply:>>585 そもそもお前はスロットサロン板で何をしている。

22

kingってものすごく頭悪いんですね。知りませんでした。がっかりです。

Reply:>>588 複素解析くらい知りている。お前に何がわかるというか。

ではkingよ複素解析について語ってくれ

Reply:>>590 Cauchyの積分定理、Cauchyの積分公式。

>>585
マルチ

>>この世は離散だから解析学は滅びるべきだよ。

ものの長さや、時間の流れは連続だが。
偏った"この世"じゃねーか？
実数の公理を使えば、コンピュータでも実数の性質を扱うことは出きるだろ。JK。

>>593
長さにも時間にもプランク単位、即ち最小単位があるだろ
どんな長さや時間もプランク単位の自然数倍、連続じゃないよ

http://ja.wikipedia.org/wiki/プランク定数
｜最近では Zurek その他の研究で、量子カオス系においてはプランク定数以下のミクロ構造が現れる事が知られており、まだプランク定数の正体はよく判っていないと言えるだろう。

>>594
　１プランク長 = 1.616252... × 10^(-35) [メートル]
って時点で、1メートルがプランク単位の自然数倍じゃないよ。
1メートルってのは実は存在しない長さなの？

ちなみにプランク質量は 0.02ミリグラム と意外にでかい

プランク単位を勘違いしてた>>594ﾌﾟｷﾞｬｰということで

>>597
ミジンコの体重がおおよそそれくらい。だからプランクトンと…

６００

６０１

>>599
座布団一枚

>>549
うん、それ無理。

ペアノの公理系で、加法の交換法則は定義されてるの。
この公理をペアノの公理系の内部で定理として証明するのは
不可能だったはずよ。

イミフ。っつーかバカ？

>>603
> >>549
> うん、それ無理。
>
> ペアノの公理系で、加法の交換法則は定義されてるの。
> この公理をペアノの公理系の内部で定理として証明するのは
> 不可能だったはずよ。

ゴルァ、シレっとウソつくんじゃねえｗｗｗｗｗ

『ペアノ数の概念について』（小野勝次・梅沢敏郎 訳・解説）、共立出版
のp.111に９という番号の付けられた

a, bεN . ⊃ . a+b=b+a

って式が定理として挙げられてるぞ。ペアノ自身の証明はそれを見ろ。

機械に証明が出来ないなら
脳は分子機械に過ぎないのだから
証明は心霊現象になってしまう

自動定理証明
http://ja.wikipedia.org/wiki/%E8%87%AA%E5%8B%95%E5%AE%9A%E7%90%86%E8%A8%BC%E6%98%8E

にでてる「ハーブランド賞」てエルブランじゃね？

>>607
Herbrandの仏語の音をカタカナで近似すれば「エルブラン」、
英語読みした音をカタカナ書きすれば「ハーブランド」

polytypic programming　in coqに載っている以下の例
Coqのバージョン8.2ではコンパイル出来ないんですが
なぜだかわかる方居ますか？
このPDFはかなり面白そうな感じがするんですが
実際に動かせないので悲しいです
別のバージョンだと動いたりするんでしょうか

Fixpoint tupleT (A:Type) (n:nat) : Type :=
match n with
| O => unit
| S m => A * tupleT A m
end.

全般的に依存型に関する情報が少ないもので困ってます

>609
Open Scope type_scope.
の１行を最初に書くと私の環境ではコンパイルとおりました。

Coq 8.1pl2 と8.2 でコンパイルが通ったことを確認しました。

>>581
ベジータ「数学は科学基礎だ!!
舐めるなよー!!!!｣

>>595
宇宙→銀河系→太陽系→惑星→分子→原子→素粒子→クォーク→…
無限階層説があるのう｡

>>610
動きました!
諦めかけてたのですが、ありがとうございます!

http://twitter.com/ranha/status/2528880672

ブラクラ危険

「gallina coq 勉強」でググったらこんなの見付けた！
定理証明支援系と依存型プログラミング勉強会
ttp://tzik.homeunix.net/ap2007/wiki/index.php?%E5%AE%9A%E7%90%86%E8%A8%BC%E6%98%8E%E6%94%AF%E6%8F%B4%E7%B3%BB%E3%81%A8%E4%BE%9D%E5%AD%98%E5%9E%8B%E3%83%97%E3%83%AD%E3%82%B0%E3%83%A9%E3%83%9F%E3%83%B3%E3%82%B0%E5%8B%89%E5%BC%B7%E4%BC%9As

>>1
> コンピューターによる定理の自動証明
> これが可能になったら数学者という仕事が無くなっちゃうの？

1 にマジレスすると、自動証明できる空間は非常に小さくて、ほとんど意味が無い。ということが証明されている。
むしろ多くのひとが興味のあるような命題は機械の支援に加え人間の手が必ず必要になる。
これは普通の数学だとあんまりうれしくない事実だけど、コンピュータの動作の保証が得られることは、プログラムの世界では
非常に重宝される技術。例えば、原子力施設のプログラムや、鉄道や道路の信号のシステム、医療、金融関係のシステムは不具合が許されない。

結論を言うと、定理証明の技術が発展すれば、数学者はプログラムの基幹システムにおいて、むしろ必要不可欠になる。
だから、数学者はプログラム技術を、プログラマは数学をしっかり学んでおくと将来お徳だと思う。

以上が私の妄想。

だれか超現実数全体が有理数全体より大きいことの証明を教えてください。

実数は超現実数の範囲で表せる
実数の集合は有理数の集合より大きい濃度を持つ

四年一時間。

coqの質問はここでいいでしょうか？

よくある論理パズル（正直者と嘘つきがいて、ある人が〜と言った。とかいうやつ）を
coqで解きたいと思ったのですが
要するに命題論理の式をCNF(乗法標準形？）に変形できればいいのですが
coqでうまくやる方法をご存知の方いますか？

>>620 命題論理のCNFへの変換のような問題であれば、証明器でなくてもプログラムで実装できると思います。

>>620 その変換の実装の正しさを検証するのであればCoqは非常に適していると思います。

はい、そういう検証もたいへん興味をそそられるのですが、
元の質問の動機は、スマリヤンの本の序盤のパズルを
覚えたてのcoqを電卓がわりに使って解けないかというぐらいのものなので、
ちょっと問題が大きい感じです。
hnfというtacticが標準であるので、
他の標準形にもちょいちょいと直せないものかと思った次第です。

>>623 スマリヤンの本をよく知らないのですが、どのようなパズル問題ですか？

>>624
Wikipediaにまとめがありました。
http://en.wikipedia.org/wiki/Knights_and_Knaves
日本語なら
http://www.kai.ed.jp/math/gakusyuu/2002minami.htm
というのが検索で出てきました。

よくあるパズルとか書きましたが、
スマリヤンがオリジナルなのかもしれません。

てｓｔ

どうも、「ＥＵＲＭＳ（∋ M_SHIRAISHI氏 ）の理論」のほうが正しいようだな。

例えば、《仮言三段論法の原理》は、従来は、 [(Ｐ⊃Ｑ)＆(Ｑ⊃Ｒ)]⊃(Ｐ⊃Ｒ) で
表わされるもののことと考えられていたのだっただが、これは、どうやら、誤りだった
ようだ。

そして、ＥＵＲＭＳの言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)]＆[Ｑ(ｘ)⇒/x/Ｒ(ｘ)］⇒/p,q,r/［Ｐ(ｘ)⇒/x/Ｒ(ｘ)] 1{Ｑ」
こそが、《仮言三段論法の原理》を 正しく捉(とら)えてたものと考えられる。

ＥＵＲＭＳの主張する「論理＊大＊改革」は、恐らく、世界を席巻することとなろう。

　　　　http://www.age.ne.jp/x/eurms/RONRI-J02.html#E-Books

806

>>596
1年前のレスだが、1mがプランク長の整数倍じゃないのは誤差だから。

電荷1Cも電気素量の整数倍じゃない。1.5倍とかなら素量として使えないが指数表現レベルなら
厳密な整数倍じゃないのは単なる誤差

そのうちクーロンの定義が素電荷の整数倍になるかも

プランク長が最小の長さならルベーグ測度は無意味じゃない？

>>632
それを言うならば、そもそも選択公理を用いた数学で物理理論を記述してるのがナンセンスなのだが
フルスペックの選択公理はBanach-Tarskiのパラドックスを導いてしまうからね

>>631
うん、例えばクーロンの定義が電気素量ｅの１Ｎ（アボガドロ数）倍（つまり１モルの陽子の電荷総量）なら明解なんだけどね
現在は電流単位としての１Ａ（アンペア）をその電流が流れる電線の間の力の強さで定義して
１Ａの強さの電流で１秒流れる電気量を１Ｃ（クーロン）として定義してるからなあ

質量の単位のｋｇについても今のキログラム原器なんて怪しげというか恐ろしく原始的な定義じゃなくて
炭素１２原子核の質量の１Ｎ倍を１２グラムとして定義しようというアイデアはかなり昔からあるんだよな
あるいは陽子（普通の軽い水素の原子核）の質量の１Ｎ倍を１ｇと定義すればもっと明解だな
炭素１２原子核にしろ陽子にしろ、そういうものの質量なら質量分析器を用いて極めて精密に測れるからね
今は逆にアボガドロ数の定義として１２ｇの炭素１２に含まれる炭素１２の原子数を用いていたんじゃないかな
（つまり上の新しい定義の提案だと、アボガドロ数は実験で決まる定数でなく最初から値を定めておく定数にせねばならない）

科学的で合理的な単位系はプランク単位系。もっというなら数値も16進数が合理的。（プランク単位系でなおかつ16進数）
10進数は人間の指の数が起源だからある意味原始的。日常生活での16進数への移行は難しいが

プランク単位系には物理的な裏付けがあるが、
数はどの底をとっても恣意的でしょう。
もっというなら16進数よりは2進数のほうが本質だと思う。

e進法ができないのは不便だな。角度だってラジアンのほうが数学的に便利だから数学では度数法に取って変わったわけだし

一進数、つまり数の個数分だけ１でも何でも良いから記号を書き並べる
のが本質。但しこれだと０を表すことができないので、
個数に１個げたを履かせることで回避するようなことをしなければ
ならない。
たとえば
０：　×
１：　××
２：　×××
１０：　×××××××××××
。。。。

それだと何かの数の整数倍しか表現できなさそうだけど、どうかな。

底とかナシで無限個のシンボルをつかって表現するのが本質なんじゃない？
つまりどの数も違うひとつの記号で表されるって感じで。

実際は、これを実現するのが無意味に大変だから、
「わかりやすい」とか「つかいやすい」とかの>>635のいうところの恣意的な理由で
適当な基数をきめて、その組み合わせやら式やらの一定のパターンでもって
数を表現しているわけだよね。（ここは「数学」の本質かな）

１進なら個体の数が直接的にわかりやすいから、
２進ならコンピュータであつかいやすいから、
１０進なら人間にわかりやすいから、
１６進ならコンピュータであつかいやすくて人間にもそこそこわかりやすいから、
という感じ？
こう書くと、この中では１６進が一番恣意的だな。

ハル　これを証明してくれ。
ハル　これは。。。。。。。。自明だ。QED

mizarやcoqの入門書とかないもんかね

スーパーコンピュータで入試問題を解答できるか

「それならコンピュータに解法プログラムと数式処理プログラムと人工知能を組み込んで問題を解かせることは
可能だと思われますか。もしできるなら、スーパーコンピュータのサーバーサイドに入試問題解説ソフトウェア
を組み込んで富士通のクラウドサービスで配布すれば教育費が安上がりになるはずです。」
http://ameblo.jp/wadahideki/entry-10502592674.html

コンピューターによる定理の自動証明
http://science6.2ch.net/test/read.cgi/math/1126017312/
職業教育訓練用クラウドサービスをお願い。安い通信教育で学べるシステムが必要。
http://jp.fujitsu.com/about/journal/voice/enq/enq1003.shtml

coqの入門書はCoqArtがあるじゃない
あとプログラマ向けにhttp://adam.chlipala.net/cpdt/とか

Coq'Art売ってねぇじゃねぇか
どうせ本屋に取り寄せて貰っても同じだし、直接springerから買うか…

プランク定数ってフォトンでやったときだろ。クオークだったら話が変わるぞ。

たいとるが　コンピューター君による自演スレ　にみえたW

＞コンピュータに解法プログラムと数式処理プログラムと人工知能を組み込んで問題を解かせることは
＞可能だと思われますか。

計算量理論などの結果からすると難しいと思うが入試問題の解法アルゴリズムについて
考察することは興味深いな。定理証明技法に基づく入試問題攻略本が書けたら売れるだろうな。

工学部の受験は自作AI持ち込みありにするべきです

HAL。。。２もんめをとけ
ボーマン。。。アンテナがへんだわ、ちょっとみてきて

適当なxを生成して、その中から「xは論理式Aの証明である」が真になる物を探す

age

これだけ出来ないと思っている人が多いということは、
俺にできるチャンスがあるってことだ。
成功したら報告しに来るよ。

プログラムが将棋におけるボナンザのように、証明の定石を沢山参考にして
学んで、その結果かなりの定理が自動的に証明できるレベルに達したとする。
だが、如何なる命題を定理に据えて理論体系を構築するのかという部分は、
どうするのか？何が定理として相応しいか、何が単なる証明できる命題という
だけの単なる命題にすぎないのかをどう判定判別するのであろうか？

607