コンピューターによる定理の自動証明
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2005/09/06(火) 23:35:120153１３２人目の素数さん
2005/11/10(木) 20:58:370154１３２人目の素数さん
2005/11/10(木) 21:18:05そういった内容は認知心理学でいうメタ知識に相当するから、
いわば「公理の公理」としておさえておくことが好ましい。
0155１３２人目の素数さん
2005/11/10(木) 22:11:500156１３２人目の素数さん
2005/11/11(金) 17:49:54どういう人に？
0157１３２人目の素数さん
2005/11/12(土) 07:28:140158１３２人目の素数さん
2005/11/12(土) 17:40:120159１３２人目の素数さん
2005/11/12(土) 17:44:110160１３２人目の素数さん
2005/11/13(日) 15:22:480161１３２人目の素数さん
2005/11/16(水) 20:43:05コンピュータに足りないのは定義を増やすという操作なわけだよ
0162１３２人目の素数さん
2005/11/18(金) 07:41:450163１３２人目の素数さん
2005/11/18(金) 07:44:370164１３２人目の素数さん
2005/11/18(金) 07:50:480165１３２人目の素数さん
2005/12/12(月) 18:46:270166１３２人目の素数さん
2005/12/12(月) 19:03:53５０年位前に計算機科学の有名な学者が１０年以内に定理の
自動証明が出来るだろうと予言した。だから専門家といってもなーんも
分かってないんだよ。現在だって同じ。
0167１３２人目の素数さん
2005/12/12(月) 22:52:38定理を全て証明していくつもり、、だったんだろうかな
何の見積もりを間違えたんだろう？
実際の定理の複雑さか計算機のスピードか
0168１３２人目の素数さん
2005/12/13(火) 09:31:57ま俺は専門家じゃないからあてにならないがｗ
今のコンピュータというのは原理的には５０年前と同じ、
つまりノイマン式。これをいくらいじっても無理だろう。
0169１３２人目の素数さん
2005/12/13(火) 14:34:14しかし証明に携わった人間によれば、時折コンピュータが
人間以上の「知性」を垣間見せることがあるという…。
0170１３２人目の素数さん
2005/12/13(火) 14:37:46時折垣間見せるじゃ駄目だろ。俺みたいにチューリングテストに
パスしないと。
0171１３２人目の素数さん
2005/12/13(火) 17:18:150172１３２人目の素数さん
2005/12/13(火) 17:18:460173GiantLeaves ◆6fN.Sojv5w
2005/12/13(火) 22:18:300174１３２人目の素数さん
2005/12/13(火) 22:22:56talk:>>とか自動生成っぽいなとか思ってｗ
0175１３２人目の素数さん
2005/12/14(水) 09:08:39冗談通じないのね。
0176１３２人目の素数さん
2005/12/20(火) 06:34:18なんで出来ないとか主張してる奴がいるんだ？
せめて「定理 自動証明」でググれ
0177１３２人目の素数さん
2005/12/21(水) 14:46:230178１３２人目の素数さん
2005/12/21(水) 15:21:45(証明が自明な定理は除いて)出来てないから。
0179１３２人目の素数さん
2005/12/21(水) 17:38:44AIも然り
0180１３２人目の素数さん
2005/12/21(水) 22:49:10暗号だけじゃなくて定理証明も。
量子コンピュータとかが実用化したら、、、？
0181１３２人目の素数さん
2005/12/22(木) 01:48:46第一コンピューターがそんなに早かったら
気象学も分子生物学も量子化学も今より進歩してるはずだよw
0182１３２人目の素数さん
2005/12/22(木) 10:42:150183１３２人目の素数さん
2005/12/22(木) 11:28:53コンピューターが何かわかっていない。考える機械だとでも
思っているのか。人間が作ったソフトウェアを実行するのみ。
計算とかは得意だから全部計算してみるとか、数え上げるなんて
ことはできるだろう。いずれにせよ有限個のみ。
0184１３２人目の素数さん
2005/12/22(木) 21:44:130185１３２人目の素数さん
2005/12/22(木) 23:19:51今までに書かれた全ての数学の論文、書籍を論理過程の
省略を無くして書き直したとしても、使われる文字の
総数は有限個に過ぎない。「任意の実数に対して成り立つ」
とかいう有限個の文字の思考で無限個のことが分ったつもり
になっているに過ぎない。
コンピュータによる定理の自動証明は可能と言ってよい。
ただコンンピュータの速度が飛躍的に増大すればいい。
証明された定理のうち、人間にとって意義あると思われる
ものを選び出すのは人間の仕事となるだろう。
コンピュータが脳と「同様に」働かなくても良い。脳が証明する
のと「同じ」定理を噴出しつづければばいい。
「ピッチングマシンが人間の投手と「同様に」働かなくてもいい。
人間が投げるのと「同じ」タマを発射すればいい。」
というのと同様。
0186１３２人目の素数さん
2005/12/23(金) 06:41:52＞ものを選び出すのは人間の仕事となるだろう。
そんな100億（くらい少なけりゃまだ良いがｗ）の芥の中から
1個の宝石を選び出す仕事が成立すると思うのかねｗ
数学者の人生の99%は無意味な定理の吟味に費やされるぞｗ
0187１３２人目の素数さん
2005/12/23(金) 08:05:42これはいいとしても
>「任意の実数に対して成り立つ」
>とかいう有限個の文字の思考で無限個のことが分ったつもり
>になっているに過ぎない。
実際どんな実数ほうりこんでも「任意の実数に対して成り立つ」
定理はなりたつでそ。しかも証明までされてるんじゃ文句言えない
でしょ。あなたは数学の証明で使われる論法はでたらめだと言いたい
のですか。コンピューターで片っ端から数を代入しても成り立つ
はずです。でもコンピューターでは有限の数しか扱えないので
無理数は扱えない。この辺がコンピューターの限界。
0188１３２人目の素数さん
2005/12/23(金) 08:13:55これも科学者の作り出した単純な世界観にすぎない。
こんなもので普遍的に正しいものが捕らえられるだろうか。
進化論を全員まじめに信じるのは日本人だけで、科学先進国
欧米ではそんなこと全然ないということは知っておくべき。
0189１３２人目の素数さん
2005/12/23(金) 08:47:05でたらめじゃなくて、有限個の文字で表現できる思考で
無限のことを考えて、その程度の思考でとらえられる
無限のからむ真理ぐらいまでしか分っていないと言って
るの。
人間が無理数を考える思考も、ある様式に則って表現
すれば、有限個の文字で表されるだろ。それをコンピュ
ータで扱うことも出来ることになるという筋。
これぞ記号論理の原理のひとつでしょ。これを拒絶する数
学屋が多い（？）のは不思議。
0190１３２人目の素数さん
2005/12/23(金) 08:47:28代数的数なら頑張れば扱える気がするけどね
扱い方工夫すれば
>>188
＞進化論を全員まじめに信じるのは日本人だけで、科学先進国
＞欧米ではそんなこと全然ないということは知っておくべき。
欧米で進化論を真っ向から否定するのは、
プロテスタントの狂信者くらいしか居ない訳ですが、、
進化論は間違っている、なぜなら聖書に書いてないから、とか物凄く
「科学的」なことを言う人たちね
とりあえずおまいさんは「利己的な遺伝子」嫁
話はそれからだ
0191１３２人目の素数さん
2005/12/23(金) 08:55:10近似値としての無理数以外扱えない。無理数の近似値
は有限の数、すなわち有理数のなかで有限のものだけ
しか正確には扱えない。これで様子を調べるとか近似値
を求めることはできる。科学実験ではそれで十分かも
しれないが数学はそういう立場ではないでそ。
0192１３２人目の素数さん
2005/12/23(金) 09:02:15>プロテスタントの狂信者くらいしか居ない訳ですが
こういう風にカルトしか単純な科学的世界観を否定しない
などと思っているのは日本以外の文化を知らないから。
ニュートン力学の神も仏もない世界観に対する議論は
さんざんされて、結局一部の狂信的な科学信奉者以外
受け入れてはいない。ニュートンに代わってアインシュタイン
がもてはやされる理由はこのあたりにもある模様。
0193１３２人目の素数さん
2005/12/23(金) 09:07:34比較的簡単に見付かる。
0194１３２人目の素数さん
2005/12/23(金) 09:09:49修正。「記号論理の原理」じゃなくて「記号論理の効用」
原理は別にある。
>>191
そう言う次元の話じゃないの。「記号論理の原理」について
１０冊ぐらいの本で１０ヶ月ぐらいかけて考えてくれ。留年
覚悟で。尤も、本人に時期が来てないなら、それでも分らん
だろうが。
分らなくてもいい。走りの原理が分らなくても走れれば
素晴らしいから。
0195１３２人目の素数さん
2005/12/23(金) 09:11:12＞ttp://www.gakushuin.ac.jp/~881791/d/0508.html#15
>>192
＞ニュートン力学の神も仏もない世界観に対する議論は
＞さんざんされて、結局一部の狂信的な科学信奉者以外
＞受け入れてはいない。
世界観は兎も角としてニュートン力学自体は受け入れているんでしょ
アインシュタインは別にニュートン力学が根本的に間違っていることを示したんじゃなくて
エネルギーが高い場合に出来る誤差を修正した、と考えるべき
大体科学と言ったって、究極的には、そう考えるのが最も尤もらしい、という以外の
根拠なんて無いんですよ
実験環境を整えてある実験をしたところ99回とも同じ、面白い結果が出た
で、100回目に同じことをしたら、やはり同じ結果が出るだろう、と推測するのが科学
いや、そうとは限らない、と考えるのが哲学
0196１３２人目の素数さん
2005/12/23(金) 09:12:500197１３２人目の素数さん
2005/12/23(金) 09:15:080198１３２人目の素数さん
2005/12/23(金) 09:20:28同じ実験をして違う結果がでると実験屋さんたちは認めないんでしょ。
数学の反例みたいなもんで。現実はわからんのをいいことに捏造なんか
もあるかもしらんが。
0199１３２人目の素数さん
2005/12/23(金) 09:38:51うわっ
コンピュータ上で無理数を表しちゃったよ。どうしよう
0200１３２人目の素数さん
2005/12/23(金) 09:42:04意味が分からん
理論屋さんでも同じ環境で違う結果が出るのを認めるのは量子論くらいじゃないかな
0201１３２人目の素数さん
2005/12/23(金) 11:44:31皮肉なのかマジなのかわからん。
計算可能な実数と不可能な実数があって、ルート２は計算可能だそうだ。
いずれにしてもこのスレの本筋からずれている話だとは思うが。
0202１３２人目の素数さん
2005/12/23(金) 11:48:15論理的な議論なら、記号論理に乗せられて、
コンピュータに乗せられるだろう。
0203１３２人目の素数さん
2005/12/23(金) 13:20:34計算可能ってどういう定義？
そういえば計算可能解析学とかあったね
かなりマイナーな分野だけど鴨さんとかそっち系の分野だったはず
0204１３２人目の素数さん
2005/12/23(金) 22:28:15コーシー列の中でアルゴリズムが定義可能なものの集合、
なんちゃってそんな安直なモノのわけないね（＾＾）
でもいかにも数学界から相手にされない分野という感じだね。
0205１３２人目の素数さん
2005/12/23(金) 22:50:40「計算不可能」を「計算可能でない」に直したい。
0206１３２人目の素数さん
2005/12/23(金) 22:53:350207１３２人目の素数さん
2005/12/23(金) 23:07:22その実数の定義が、有限の長さの、意味の
はっきりした文または式によって記述されて、
しかも、その記述に基いて、その実数の
数値を、任意の精度で有限時間内に算出できる
ことが最低限必要なのだそうだ。
すると、そういう実数は可算個しかないのだ
そうだ。
円周率も、自然対数の底eも、ルート２も、
計算可能な実数であって、確実に「有る」と
言える数なのだと。
0208１３２人目の素数さん
2005/12/23(金) 23:16:44行き交うには、このあたり（チューリングの計算可能な
実数とか）を連結器にするしかないか。いずれの人に
とっても、最大の関心事というわけではないだろうが。
0209１３２人目の素数さん
2005/12/24(土) 06:04:25a(n)が計算可能函数（つまり全域再帰函数でいいんだっけ？）
となること、というのが定義か
でもそういう実数は計算可能というより定義可能とでも行った方が良いんじゃない？
0210１３２人目の素数さん
2005/12/24(土) 11:34:05そもそも計算不可能な命題がある事も自明なんだから特に問題はないとおもう
0211１３２人目の素数さん
2005/12/24(土) 11:40:02導出できた定理が現在の学会の流行り廃りを考慮した上で価値のある定理かどうかを
AIが判断するのは無理があるだろうな
0212１３２人目の素数さん
2005/12/31(土) 19:55:39色仕掛けを使う、おべんちゃらを言う、
こういった知性がAIに備わり、孫氏などの計略をも学べば
危うからず。
0213１３２人目の素数さん
2006/01/02(月) 05:35:170214１３２人目の素数さん
2006/01/05(木) 21:47:52どうやってそれを読んで理解し納得できるというのだろうか？
0215１３２人目の素数さん
2006/01/05(木) 21:55:44今から２５年以上前か…。
0216１３２人目の素数さん
2006/01/05(木) 21:56:470217１３２人目の素数さん
2006/01/08(日) 03:41:06ゲーデルも、真理に到達するには科学的世界観だけではダメで、神学的世界観も
必要だと考えていたらしい。
来世は存在する。来世が存在しないとしたら今いるこの世界にも意味がないのだそうだ。
この本に書かれていた。
http://bookweb.kinokuniya.co.jp/htm/4535782598.html
0218１３２人目の素数さん
2006/01/08(日) 13:40:160219１３２人目の素数さん
2006/01/09(月) 00:46:35ゲーデルの考え。
ゲーデル 竹内外史著 日本評論社
pp.178-179
もしこの世界が理性をもって構成されており、意味をもっているとするならば、
来世の再会は存在するにちがいありません。なぜならば、自分自身の発展および
人々との関係に無限の可能性をもっていながら、その千分の一も達成できない
人間という存在を創るということに、いったい何の意味があるでしょうか。
それはちょうど細心の注意と莫大な費用をかけて家の基礎を作り、それからそれを
無駄にしてしまうようなものです。しかし、この世界が理性をもって構成されていると
信ずる理由があるでしょうか？ 私はあると信じます。なぜならば、この世界は決して
混乱したものではなく、またどうでもよいというものでもなく、自然科学が示している
ように、いたるところに整然とした秩序があります。秩序というのはまさしく理性の
一つの形態です。
p.183
私は宗教のなかには一般に信じられているよりはるかに多くの理性があると信じています。
もっとも教会のなかにはありませんが。しかしわれわれは若いときから、学校で、
悪い宗教教育によって、また本や経験によって、そうでないと偏見をもつように教育
されています。
0220219
2006/01/09(月) 00:51:20p.184
われわれは来世ではこの世での経験を覚えている。実は来世までは本当にその経験の
意味は理解していない。したがってわれわれのこの世での経験は来世で学ぶための
素材にすぎない。
p.185
もし、この世の経験を来世で覚えていることは不可能だという反対があっても、来世では
潜在した記憶をもって生まれてくる可能性があるということができます。その上、来世では
われわれの心の状態は現世よりはるかによく、したがって来世では、主要なことのすべてを
2×2＝4のように絶対に誤らない正確なこととして認識するだろうということを仮定しな
ければなりません。
pp.188-189
私が神学的世界像と呼ぶものは、世界とその内のすべてのものが意味と理性をもっている、
そして正しい疑問の余地のない意味をもっている、という思想です。そしてこの考えは
ただちに次の結論に導きます。われわれのこの世での存在はそれ自身きわめて疑問のある
意味をもっているにすぎないから、それは来世の目的のための手段でしかあり得ない。
さて、この世のすべてのものは意味をもっているという思想は、すべてのものはその原因
をもっているという原理と正確に対応するものです。そしてこの後者の原理はすべての
科学の基礎となっているものです。
0221219
2006/01/09(月) 00:58:04竹内氏のコメント
p.178
ここに出てくるゲーデルは私のよく知らないゲーデルである。しかしこれもゲーデルの
一面である。神学や哲学でのゲーデルの考えは私などには分かりかねるが、それでも
彼の数学での考え方といろいろなつながりが認められる。
0222１３２人目の素数さん
2006/01/10(火) 00:20:54命題Mの証明が可能であるならば、そのような証明のうちで最も
記述が短い証明が存在する。この長さをL(M)としよう。
もしも、ある命題M1に対してその証明があったとして、
仮にその最短な証明の長さL(M1)が10＾100とかであったならば、
そのような命題は現実的には書き下すことが出来ないし
（なぜなら宇宙の原子の個数を越えている）、もちろん読み通す
こともできないであろう。10＾100ほどではなくても10＾10であっても
相当に困難であるが、計算機の容量と速度を持ってすれば格納したり
スキャンしたりすることは可能である。
0223１３２人目の素数さん
2006/01/10(火) 00:25:56各人が個人として行わねばならないとしたら、L(M)が比較的小さいような
命題Mしか（一生をかけるとしても）現実問題としては取り扱うことが
出来ないのである。一人でやるという立場を放棄して、１００人の集団で
分担して証明を書いたり、チェックする、そうしてトップダウン的に
証明のプロセスを分解して部分に分けて、、、と系統的証明が行えるならば
（証明の記述長は幾分長くなるかもしれないが）100人力となり、100倍長い
証明もあるいは検証できるようになるかもしれない、また１万人でなら
１万人力になるかもしれない。しかし人数が増えると次第に誤りが混入する
リスクが高まるので、独立な複数のグループに並行的に検査させたりするほか
本当にチェック機能が働いているかあるいはメクラ判を押していたりしないか
を確かめるためには、わざと証明の一部に誤謬を混入させてそれを検出するか
どうかを二重盲検検査する必要があるだろう。証明行為の過程自身の誤動作
を問題としなければならないからだ。
0224１３２人目の素数さん
2006/01/10(火) 00:46:42ことはできないだろう。さらに数世代に渡って証明を検証するということが
考えられる、代々証明に取り組んで１０世代前から取り組んだ検証がまもなく
終わろうとしている、、、、というような具合にだ。
だが、やはり10＾100程度のところに限界があるに違いない。
全数検査しかないような問題であれば、10＾100はおろか10＾10000のような
問題であっても容易に作れる。
このような有限行為の立場からは、命題とは何か、証明とは何か、という
疑問が沸いてくる。
0225１３２人目の素数さん
2006/01/10(火) 00:56:11記号系というのは、命題にあわせて拡張されるもので、L(M)のような
関数は大した意味を持たないのではないか。
実際、複雑な数学を多くの人が理解できるようになったのは、記号の
整備によるところが大きいわけだし。
0226１３２人目の素数さん
2006/01/10(火) 02:39:200227１３２人目の素数さん
2006/01/10(火) 02:52:21先祖が姉歯秀次
0228１３２人目の素数さん
2006/01/10(火) 07:58:36１｡恒真式の生成
２｡論理変数と事象の結びつけ
に帰着するのでは、、
0229１３２人目の素数さん
2006/01/13(金) 03:01:31自動証明をするためには少なくとも体系が決められていなければならない（言語や公理など）。
しかし、数学者はしばしば、新しい対象扱うために、それまで存在しなかった
新しい体系を導入して、そこで考える。そういう体系自体を新たに定義するような行為
は人間にしか出来ないのではないか？
0230１３２人目の素数さん
2006/01/13(金) 05:06:140231１３２人目の素数さん
2006/01/13(金) 12:45:06証明されています：
いかなる数学的問題でも
機械的計算で解決できるような
コンピュータ-プログラムは、
作れない。
0232１３２人目の素数さん
2006/01/13(金) 13:33:410233１３２人目の素数さん
2006/01/13(金) 13:59:410234１３２人目の素数さん
2006/01/13(金) 14:08:14自動証明が出来るためには（たとえそれが”全て”の証明を網羅できないにしても）
まず体系自体を一つ与える必要がある。
体系を与えればその体系内で成り立つ可算個ぐらいの証明を
自動的に得ることが出来る。
しかし、どう考えてもその課程で、新たな
数学的に興味のある体系そのものが自動的に出てくることは
考えられない。
0235１３２人目の素数さん
2006/01/13(金) 14:25:14いかなる数学的問題でも解決できる数学者が存在するわけではないし。
0236１３２人目の素数さん
2006/01/13(金) 14:52:28Aを行う者にBを行うことはできそうもないので、Bを行う者は存在しない?
電卓ソフトで文書作成はできそうもないので、文書作成をするためのソフトは存在しない、とか。
0237１３２人目の素数さん
2006/01/13(金) 15:17:20文献：前原昭二『数学基礎論入門』朝倉書店
また、ゲーデルの不完全性定理に関するスレッドにも、
関連するコメントがあります。
0238１３２人目の素数さん
2006/01/13(金) 15:29:460239１３２人目の素数さん
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そんなのサイコロを上手く定義して、6つの場合に場合分けして考えれば
証明できるんでは？
0244１３２人目の素数さん
2006/01/14(土) 12:18:41時間が無限にあれば絶対に見つけられるよ。
リウビルの定理を用いた基本定理の証明も当然できる。
効率よく見つける方法は分野の相違に関係なく難しい。
計算機は分野の認識なんかしない。（させようとしなければ）
0245１３２人目の素数さん
2006/01/14(土) 13:37:05自然数を含む命題論理の成否を決定するアルゴリズムは存在しない。
0246１３２人目の素数さん
2006/01/14(土) 16:34:18○○作成ソフトの○○が１００年後に発見される概念だったら
現時点で○○作成ソフトは作れない。そして○○を発見するという
仕事が数学者に残される。その様な○○はいくらでもありそうなので
数学者の仕事はなくならない、・・・というはなし
0247１３２人目の素数さん
2006/01/14(土) 17:34:43コンピュータに新しい概念を発見することはできないと思う理由は?
発見できそうもないと>>246が思うから発見できるはずがない?
0248１３２人目の素数さん
2006/01/14(土) 19:16:18>>244 は定理の集合が帰納的可算だってことを言ってるだけじゃないの？
0249１３２人目の素数さん
2006/01/14(土) 20:44:00それって新しい概念だって人間が見て判断できることなのかね
0250１３２人目の素数さん
2006/01/14(土) 21:18:32数学的に価値のある体系自体の数え上げが可能ということですか？
そうなると本当に、数学者要らないですね。”独創的”なんていう概念も意味がないことになるし、・・・
0251１３２人目の素数さん
2006/01/14(土) 21:23:30体系そのものをコーディングして（何らかの数を対応ずけて）
数学的に価値ありという概念を式で表して、（これは矛盾しなければ価値ありとしていいのかどうかは良く分からないけど・・・）
その様な数の全体が計算可能かどうかを考えればいいのかな・・・
・・・まあ、どっちの結果にしろ自明じゃないことは分かるわｗ
0252１３２人目の素数さん
2006/01/14(土) 21:26:34■ このスレッドは過去ログ倉庫に格納されています