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

0001１３２人目の素数さん

2005/09/06(火) 23:35:12

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

0237１３２人目の素数さん

2006/01/13(金) 15:17:20

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

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

0238１３２人目の素数さん

2006/01/13(金) 15:29:46

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

0239１３２人目の素数さん

2006/01/13(金) 15:39:33

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

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

0240１３２人目の素数さん

2006/01/13(金) 18:35:07

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

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

0241１３２人目の素数さん

2006/01/13(金) 21:05:30

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

0242１３２人目の素数さん

2006/01/13(金) 21:44:58

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

0243１３２人目の素数さん

2006/01/14(土) 04:50:28

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

0244１３２人目の素数さん

2006/01/14(土) 12:18:41

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

0245１３２人目の素数さん

2006/01/14(土) 13:37:05

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

0246１３２人目の素数さん

2006/01/14(土) 16:34:18

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

0247１３２人目の素数さん

2006/01/14(土) 17:34:43

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

0248１３２人目の素数さん

2006/01/14(土) 19:16:18

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

0249１３２人目の素数さん

2006/01/14(土) 20:44:00

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

0250１３２人目の素数さん

2006/01/14(土) 21:18:32

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

0251１３２人目の素数さん

2006/01/14(土) 21:23:30

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

0252１３２人目の素数さん

2006/01/14(土) 21:26:34

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

0253１３２人目の素数さん

2006/01/15(日) 16:51:59

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

0254１３２人目の素数さん

2006/01/16(月) 10:58:00

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

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

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

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

0255１３２人目の素数さん

2006/01/16(月) 11:04:33

>>219

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

0256１３２人目の素数さん

2006/01/16(月) 14:28:11

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

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

0257１３２人目の素数さん

2006/01/16(月) 15:00:40

>>256

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

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

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

0258１３２人目の素数さん

2006/01/16(月) 15:36:54

来世は人大杉だな

0259１３２人目の素数さん

2006/01/16(月) 16:46:25

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

0260１３２人目の素数さん

2006/01/16(月) 18:05:57

そこで江原さんですよ

0261１３２人目の素数さん

2006/01/16(月) 22:38:27

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

0262１３２人目の素数さん

2006/01/17(火) 09:00:51

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

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

0263１３２人目の素数さん

2006/01/19(木) 03:46:05

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

0264１３２人目の素数さん

2006/01/22(日) 03:41:20

>>263
OMOIKOMI NO HAGESHII YATSUYONOO

0265１３２人目の素数さん

2006/01/22(日) 22:57:18

age

0266１３２人目の素数さん

2006/01/23(月) 22:48:57

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

0267１３２人目の素数さん

2006/01/24(火) 09:42:34

coqとか使ってる？

0268１３２人目の素数さん

2006/01/29(日) 05:19:47

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

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

0269１３２人目の素数さん

2006/02/05(日) 07:27:08

281

0270１３２人目の素数さん

2006/03/02(木) 16:59:59

367

0271中川泰秀 ◆IvNr9.tOCg

2006/03/13(月) 16:40:57

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

0272１３２人目の素数さん

2006/03/14(火) 04:35:18

age

0273１３２人目の素数さん

2006/03/14(火) 14:46:41

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

0274中川秀泰 ◆IPeKUwqiHM

2006/03/14(火) 14:50:55

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

0275BW of Tama King

2006/03/14(火) 14:54:52

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

0276GiantLeaves ◆6fN.Sojv5w

2006/03/14(火) 15:00:04

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

0277BW of Tama King

2006/03/14(火) 15:01:30

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

0278中川秀泰 ◆IPeKUwqiHM

2006/03/14(火) 15:07:02

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

0279GiantLeaves ◆6fN.Sojv5w

2006/03/14(火) 15:36:00

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

0280BW of Tama King

2006/03/14(火) 15:45:12

>>279 中川さんに聞け。

0281１３２人目の素数さん

2006/03/26(日) 14:29:19

0282１３２人目の素数さん

2006/04/04(火) 22:11:13

このスレもう終わりか？

0283１３２人目の素数さん

2006/04/15(土) 23:09:20

193

0284中川秀泰

2006/05/12(金) 05:31:36

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

0285１３２人目の素数さん

2006/05/13(土) 22:25:06

521

0286１３２人目の素数さん

2006/05/14(日) 05:01:34

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

0287１３２人目の素数さん

2006/05/16(火) 15:42:02

MIZAR!

0288１３２人目の素数さん

2006/05/16(火) 16:04:34

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

0289１３２人目の素数さん

2006/05/26(金) 14:14:49

620

0290１３２人目の素数さん

2006/06/16(金) 01:05:04

912

0291１３２人目の素数さん

2006/07/28(金) 15:37:13

977

0292１３２人目の素数さん

2006/08/15(火) 04:09:52

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

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

0293KingOfUniverse ◆667la1PjK2

2006/08/17(木) 06:00:12

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

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

0294１３２人目の素数さん

2006/08/30(水) 16:55:54

648

0295１３２人目の素数さん

2006/10/03(火) 00:21:38

174

0296１３２人目の素数さん

2006/11/12(日) 23:47:29

968

0297１３２人目の素数さん

2006/12/07(木) 20:24:25

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

0298１３２人目の素数さん

2006/12/07(木) 20:38:28

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

0299１３２人目の素数さん

2006/12/07(木) 20:52:47

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

0300１３２人目の素数さん

2006/12/07(木) 21:30:46

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

0301数学系のD1です

2006/12/07(木) 21:43:09

>299

ありがとうです

0302１３２人目の素数さん

2006/12/07(木) 23:13:55

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

0303１３２人目の素数さん

2006/12/07(木) 23:41:34

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

0304１３２人目の素数さん

2006/12/07(木) 23:42:34

こらっ

0305１３２人目の素数さん

2007/01/01(月) 00:05:23

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

0306１３２人目の素数さん

2007/02/05(月) 17:08:31

610

0307１３２人目の素数さん

2007/02/07(水) 04:18:00

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

0308１３２人目の素数さん

2007/02/07(水) 05:05:15

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

0309１３２人目の素数さん

2007/02/07(水) 11:50:21

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

0310１３２人目の素数さん

2007/02/07(水) 21:31:58

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

0311１３２人目の素数さん

2007/02/08(木) 06:28:03

>>309
逆もあるよん

0312１３２人目の素数さん

2007/02/10(土) 18:55:12

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

0313１３２人目の素数さん

2007/02/11(日) 13:27:43

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

0314１３２人目の素数さん

2007/03/11(日) 17:58:47

age

0315１３２人目の素数さん

2007/03/15(木) 23:25:07

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

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

0316１３２人目の素数さん

2007/03/16(金) 00:59:14

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

0317１３２人目の素数さん

2007/03/16(金) 04:06:48

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

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

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

0318 ◆WSu5GQQTQ2

2007/06/05(火) 12:06:21

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

0319１３２人目の素数さん

2007/06/24(日) 23:48:15

age

0320１３２人目の素数さん

2007/06/25(月) 00:28:07

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

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

0321エレガントな解答を求む

2007/06/25(月) 00:40:34

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

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

0322１３２人目の素数さん

2007/06/25(月) 13:43:13

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

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

0323１３２人目の素数さん

2007/06/25(月) 14:19:34

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

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

0324１３２人目の素数さん

2007/06/25(月) 14:21:35

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

ツンドラ気候か？って…

0325１３２人目の素数さん

2007/06/25(月) 14:28:09

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

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

0326１３２人目の素数さん

2007/06/25(月) 14:31:15

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

0327１３２人目の素数さん

2007/06/25(月) 14:35:37

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

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

0328１３２人目の素数さん

2007/06/25(月) 14:48:33

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

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

0329１３２人目の素数さん

2007/06/25(月) 15:51:51

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

0330１３２人目の素数さん

2007/06/25(月) 18:48:12

ツンデレ教会は実在する

0331１３２人目の素数さん

2007/07/01(日) 14:51:58

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

0332１３２人目の素数さん

2007/07/01(日) 21:06:28

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

0333１３２人目の素数さん

2007/07/02(月) 11:34:51

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

0334１３２人目の素数さん

2007/07/03(火) 04:00:39

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

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

0335１３２人目の素数さん

2007/07/03(火) 04:29:20

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

0336１３２人目の素数さん

2007/07/03(火) 06:07:26

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