コンピューターによる定理の自動証明
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2005/09/06(火) 23:35:120002１３２人目の素数さん
2005/09/06(火) 23:36:590003１３２人目の素数さん
2005/09/07(水) 00:22:52その時にコンピュータには出来ないような新しい仕事を見つけられなければ
数学者だけでなく殆どの人間の仕事が無くなる。
0004１３２人目の素数さん
2005/09/07(水) 00:34:23コンピュータによる定理の自動証明ってどうやるのさ？
0005１３２人目の素数さん
2005/09/07(水) 10:58:400006１３２人目の素数さん
2005/09/07(水) 12:43:47永久に出来ないだろう。
0007１３２人目の素数さん
2005/09/07(水) 12:53:17何が「美しい」か見極める事(新しくないけど)。
コンピュータの万能性の可能性を否定するにはそれだけで十分。
0008１３２人目の素数さん
2005/09/07(水) 13:35:030009１３２人目の素数さん
2005/09/07(水) 18:10:37それを2進であらわせれば、コンピュータに数学をやらせる土台ができるかもな～。
0010１３２人目の素数さん
2005/09/07(水) 18:13:06「美しい証明」になるかどうかは別問題。
0011１３２人目の素数さん
2005/09/07(水) 18:13:470012１３２人目の素数さん
2005/09/07(水) 18:23:540013１３２人目の素数さん
2005/09/07(水) 20:16:390014１３２人目の素数さん
2005/09/08(木) 00:23:02コンピュータによる定理の自動証明は今のところ「少し可能」という状態です。
事実、コンピュータで自動証明された定理も存在します。ただ、その証明はおせじにも美しい証明とはいえないが…
証明の内容は忘れたが、こんなことを前期の授業でやった。
0015１３２人目の素数さん
2005/09/08(木) 00:48:410016１３２人目の素数さん
2005/09/08(木) 01:31:06たしか、二等辺三角形がどうたらってやつだった
四色問題は異論があるから微妙じゃない?
0017１３２人目の素数さん
2005/09/08(木) 03:48:11その全てのパートに対して定理が成り立つことを確認する所を
コンピュータにやらせたんだったっけ？
この場合、コンピュータは人間の作ったアルゴリズム通りに動作しているだけなので、
「自動」証明とは言い難いなぁ。
てか、自動証明って何？コンピュータが1から全部証明やってくれることでしょ？
0018１３２人目の素数さん
2005/09/08(木) 07:33:41微分方程式の数値解を計算機で出すか手計算でやるかの違いみたいな感じがする。
普通の自動証明というと、推論規則と命題を与えてその証明を作らせることかな？
0019１３２人目の素数さん
2005/09/08(木) 08:47:53定理から証明に必要な公理を導き出す。
0020１３２人目の素数さん
2005/09/08(木) 11:02:02基本的には￢（公理⇒定理）から自動的に矛盾を導く。
証明が存在するなら、矛盾が導ける。
しかし、存在しない場合にはプロセスが終了しない可能性がある。
0021１３２人目の素数さん
2005/09/08(木) 16:06:50それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
例えば宇宙の原子の数なんて10^50程度のオーダーしかない。
ちょっと難しい定理の機械証明の探索論理ステップ数なんて
そんなオーダーの組合わせ数じゃ済まないんじゃないの？
0022１３２人目の素数さん
2005/09/08(木) 16:45:14そういうメタ知識を用いると、かなりよくなります。
0023１３２人目の素数さん
2005/09/08(木) 18:01:02それは人間が発見した定理を利用するということ？
それはちょっとズルイというか、やっぱ人間が必要なんじゃないかと
0024１３２人目の素数さん
2005/09/08(木) 18:03:40なんじゃそりゃ、
もしや0から全てコンピュータに行わせようとしてるのか？
過去の資産を生かさずしてどうする。
0025１３２人目の素数さん
2005/09/08(木) 18:08:21と言いたくなるな
0026１３２人目の素数さん
2005/09/08(木) 18:25:38人間がやる定理証明に役立ってくれればいいの。
なんでもかんでもコンピュータにやらせる必要は無いの。
0027１３２人目の素数さん
2005/09/08(木) 18:25:420028１３２人目の素数さん
2005/09/08(木) 18:31:02A=B？
0029１３２人目の素数さん
2005/09/08(木) 18:35:36それで役立つんかい？
人間が証明出来ない定理をコンピュータが証明してくれるとか？
0030１３２人目の素数さん
2005/09/08(木) 19:41:41正しい定理を見つける仕事は残るだろう。
0031１３２人目の素数さん
2005/09/08(木) 20:02:070032１３２人目の素数さん
2005/09/08(木) 20:08:24コンピュータなんてただ計算が速いだけだし。難しい予想なんて解こうものなら既存の数学では無理な場合もあるし、
コンピュータがその道具を作っていくなんてまず不可能じゃね？
0033１３２人目の素数さん
2005/09/08(木) 23:08:570034１３２人目の素数さん
2005/09/08(木) 23:14:100035１３２人目の素数さん
2005/09/08(木) 23:57:12エルオーネの能力に比べれば、証明なんて
0036１３２人目の素数さん
2005/09/09(金) 01:31:54強化学習も結局はx^nオーダーの計算量となるわけで
0037１３２人目の素数さん
2005/09/09(金) 01:36:530038１３２人目の素数さん
2005/09/09(金) 05:54:410039１３２人目の素数さん
2005/09/09(金) 13:21:380040１３２人目の素数さん
2005/09/09(金) 13:32:45第五世代コンピュータ開発計画とかいう税金のムダ使いで
0041１３２人目の素数さん
2005/09/09(金) 13:55:070042１３２人目の素数さん
2005/09/09(金) 14:14:590043１３２人目の素数さん
2005/09/09(金) 14:37:44と言える？
人間並みの人工知能ができれば、自動証明もできるはず。
0044GiantLeaves ◆6fN.Sojv5w
2005/09/09(金) 17:03:36検索の枝きりが難しいと思う。
0045１３２人目の素数さん
2005/09/09(金) 17:40:480046１３２人目の素数さん
2005/09/09(金) 19:04:07あっち向いて二人で前ならえ
0048１３２人目の素数さん
2005/09/09(金) 23:15:49http://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
ﾊｧ?
0049１３２人目の素数さん
2005/09/09(金) 23:30:320050１３２人目の素数さん
2005/09/10(土) 06:22:490051１３２人目の素数さん
2005/09/10(土) 10:43:48キミはgoogle の使い方を知らない。
0052１３２人目の素数さん
2005/09/10(土) 11:07:15ようだよ。
お前らが大好きな数研の教科書書いてる方が
精力的に進めている
0053１３２人目の素数さん
2005/09/10(土) 11:46:30mizarは"theorem prover"ではなく"proof checker"ですよ。
checkerでさえ現状ではライブラリ不足で実際に数学では使えないでしょう。
005448
2005/09/10(土) 13:48:10ではどのようにすればA=BでGoogleで検索できるか教えていただけますか？
(´-`).｡ｏO(二重引用符でくくれとかそういうｵﾁかな？)
0055名無しさん＠そうだ選挙に行こう
2005/09/10(土) 23:49:29005648
2005/09/10(土) 23:53:250057名無しさん＠そうだ選挙に行こう
2005/09/11(日) 19:18:21ライブラリ不足かどうかは知らんが、そもそも現実の数学研究で使えるような
表現力を持つ言語を処理させるのはきついんじゃなかろうかと思う。
>>54
俺も気になる。
「A=B」みたいなのをキーワードにしてGoogleで有意義な情報を引き出せるのか？
まあ元々の発言(>>5)の言わんとするところはわからなくもないが。
0058名無しさん＠そうだ選挙に行こう
2005/09/11(日) 22:54:00しらみつぶしで￢(0=0)の証明を探索させたら、
もしかしたら有限時間内に「証明あり」って出力が返る可能性がある?
もしそうなったらどうなるの?
0059名無しさん＠そうだ選挙に行こう
2005/09/11(日) 23:03:14PA が矛盾してるならあるかもね
0060名無しさん＠そうだ選挙に行こう
2005/09/11(日) 23:31:38こえー。そしたら帰納法使った証明が全ておじゃんだしZFとかも壊滅だし。
>>58の自動証明を延々走らせてる不信心な暇人っていないのかな。
0061１３２人目の素数さん
2005/09/12(月) 08:30:11トッパンが2000年に出版事業から撤退したため、あまり知られてない。
幸い原本がpdfで公開されている。クヌースによる序言だけでも読むことを勧める。
http://www.cis.upenn.edu/~wilf/AeqB.html
0062１３２人目の素数さん
2005/09/12(月) 17:01:24＞それはバカチョン方式でしらみつぶしに証明を探る方法でしょ。
人間もバカチョンでしらみつぶしに探してる。意識してないだけ。
人間が証明を見つけるまでの間にもそれこそ長い年月を必要としている。
今のコンピュータよりも人間のほうが優れているかもしれんが
それこそ非常に長い時間をかけた進化の結果である。
0063１３２人目の素数さん
2005/09/12(月) 17:05:14嘘だろ
0064１３２人目の素数さん
2005/09/12(月) 17:12:09残念だが本当だ。
ところで、誰かTarskiの量化記号消去について簡単に説明してくれ。
0065１３２人目の素数さん
2005/09/12(月) 17:21:28話をそらすなよ。しらみつぶしなわけないだろ
しらみつぶしだったら時間がかかりすぎ。
0066１３２人目の素数さん
2005/09/12(月) 17:34:00いや、そのくらい時間がかかるのが当然なんだ。
それより、質問したことについて知らないなら黙っててくれ。
無知な奴と遊んでる暇はないんだ。
0067１３２人目の素数さん
2005/09/12(月) 17:41:41時間がかかりすぎというのは１００年とか２００年のオーダー
じゃないんだよ。現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。
0068１３２人目の素数さん
2005/09/12(月) 17:43:51＞現に例えば俺が証明を考えてるときにしらみつぶしになんか
調べてないよ。
君以前の人がそうしている。
君がその知識を利用しているときに
そのことを意識できないだけ。
0069１３２人目の素数さん
2005/09/12(月) 17:58:40過去の知識といっても膨大。
その膨大な知識をしらみつぶしに調べてるわけじゃない。
0070１３２人目の素数さん
2005/09/12(月) 18:02:230071１３２人目の素数さん
2005/09/12(月) 18:26:370072１３２人目の素数さん
2005/09/12(月) 18:51:19それと同じで証明もこうすればよさそうだ、とある程度見切りをつけて行っているはず。
直観力+構成力+知識・経験が物を言う。
0073１３２人目の素数さん
2005/09/12(月) 18:54:43その昔のひとが得た結果の組み合わせの数だって膨大。
それを、しらみつぶしに調べてるわけない。
007471
2005/09/12(月) 19:28:09我々がそういう力を持ってるのは昔の人がしらみつぶしにやって得た知識を
受け継いでるからだと考えることもまったく不可能なわけではないんじゃない？
>>73
まあそうかもしれないとは思うけど、自信を持って言い切れる理由があるの？
一応言っとくと、>>62 を積極的に支持するわけじゃないよ。
けど、間違いだという根拠も持ってないし、
部分的には正しいように思えるからあえてこういうレスをしてみた。
0075１３２人目の素数さん
2005/09/12(月) 20:19:54それ使って証明しても「しらみつぶしで証明しました」って言うわけか？
0076１３２人目の素数さん
2005/09/12(月) 20:31:51知識があるっていうのは、経験則でこの対戦は無いってシードの部分がいくつかあって考慮する必要のない部分があるってことでしょ。
0077１３２人目の素数さん
2005/09/12(月) 20:39:100078１３２人目の素数さん
2005/09/12(月) 20:39:150079１３２人目の素数さん
2005/09/12(月) 21:35:020080１３２人目の素数さん
2005/09/12(月) 21:37:47最近使ってなかったせいか忘れていた。
0081１３２人目の素数さん
2005/09/12(月) 21:39:37ヒューリスティックスなしらみつぶしで、「知識」のデータベースを
元に計算してまつ
0082１３２人目の素数さん
2005/09/12(月) 21:43:39ﾜﾛｽw
0083１３２人目の素数さん
2005/09/13(火) 13:45:06わかっちゃいない。それをコンピュータでシミュレート出来るわけがない。
映画とかＳＦでは人間なみのロボットが出てくるけど、そんなのまさに
夢物語。人口知能の研究者ってのは鉄腕アトムの読みすぎ。
定理の証明というのは人間の知的能力の一部だけど、まるで解明
0084１３２人目の素数さん
2005/09/13(火) 13:49:550085１３２人目の素数さん
2005/09/13(火) 16:01:37＞証明もこうすればよさそうだ、ある程度見切りをつけて行っているはず
それはしらみつぶしとは矛盾しない。
単に深さ優先探索ではないというだけ。
0086１３２人目の素数さん
2005/09/13(火) 16:04:24ﾜﾛｽw
0087１３２人目の素数さん
2005/09/13(火) 16:04:25＞それをコンピュータでシミュレート出来るわけがない。
･･･というより、シミュレートしていたとしても
それに気づくことができないというべきか。
ところで数学の定理の証明がすばらしいものだ
という考えは数学をやっている人間の個人的感情
に過ぎない。
0088１３２人目の素数さん
2005/09/13(火) 16:30:30定理の証明が出来るということは不思議な能力だという考えは？
0089１３２人目の素数さん
2005/09/13(火) 16:38:48不思議とは無理解のことである。
0090１３２人目の素数さん
2005/09/13(火) 17:06:410091１３２人目の素数さん
2005/09/13(火) 17:51:05出来るのではないか。
0092１３２人目の素数さん
2005/09/13(火) 18:10:57データをどうやって入れるんだよ
0093１３２人目の素数さん
2005/09/13(火) 18:15:55そのコンピュータは自分自身をシミュレートするのか？
0094１３２人目の素数さん
2005/09/13(火) 18:53:470095１３２人目の素数さん
2005/09/14(水) 00:02:45チューリングマシン
とか
停止問題
でぐぐってみ。否定的な結論が出るから。
0096１３２人目の素数さん
2005/09/14(水) 06:20:52もし、すべての数学定理が計算機で証明できるならば、
たったひとつのアルゴリズムから、次々に定理を自動生成できるんじゃなかろうか？
そんなアルゴリズムが果たして存在するのか？
0097１３２人目の素数さん
2005/09/14(水) 07:14:49ZFC を計算機で書けばいいわけだから原理的には余裕でできる
けどなんか工夫しないと時間かかりすぎて意味のある定理はほとんど出ないと思う
0098１３２人目の素数さん
2005/09/14(水) 07:39:17くそ定理は山程合成出来る。
0099１３２人目の素数さん
2005/09/14(水) 09:30:09彼の不完全性定理を基にしている。
人工知能を研究している人なら知ってるよね？
0100１３２人目の素数さん
2005/09/14(水) 10:21:30コンピュータをシミュレーションするコンピュータはターゲットのコンピュータより
メモリは大きくスピードも速くなければならない。
0101１３２人目の素数さん
2005/09/14(水) 10:31:37全ての原子のデータなんてわかるわけがない。
可能性があるとしたらBig Bangのシミュレータ。
仮に出来たとしても地球が出来るまで相当時間がかかるｗ
0102１３２人目の素数さん
2005/09/14(水) 18:28:09確かにメモリは大きい必要があるが、
スピードに関しては遅くても構わない。
ただし、もちろん実物より遅くなってしまう。
用途によっては実物より遅くても、結果の再現が得られれば良い場合もある。
例えば新しいCPUの回路設計など。
0103１３２人目の素数さん
2005/09/14(水) 18:29:11文字通りトリビアの泉になるわけだな……。
0104１３２人目の素数さん
2005/09/14(水) 18:46:140105１３２人目の素数さん
2005/09/14(水) 19:38:13「定理」は有限文字列で表現できるから
「この世のすべての定理」を列挙することは一応できるけど
それらすべての真偽を判定することはできないと言うことか。
0106１３２人目の素数さん
2005/09/14(水) 22:21:08証明できないものを定理とは呼ばないんじゃ？
それでも定理全てを列挙することは出来るが。
0107１３２人目の素数さん
2005/09/14(水) 22:29:02ルールや対局データを与え、アマチュアには勝てるようにプログラムされている。
自動証明も同じようにできそうだけど、案外自動証明を研究されている方がプログラミングが不得意なのかもしれないよ。
私の従兄弟は数学のセンスは凄いのだけど、プログラムはてんで組めないんだよね。
0108１３２人目の素数さん
2005/09/14(水) 22:34:56ゴメンナサイ。「定理」ではなく「命題」と言うべきでした。
0109１３２人目の素数さん
2005/09/14(水) 22:41:570110１３２人目の素数さん
2005/09/14(水) 22:49:06自動証明は将棋みたいに特化したものじゃないから同じようには無理だと思うよ。
あと数学のセンスとプログラム組む能力は関係ないと思う。
そもそもプログラムと一括りにしているが、使う言語がCかLispかでも
だいぶ違うんじゃないか？
ちなみに俺の友達には、高校数学のアルゴリズムの項目は
BASICじゃなくて関数型言語を使うべきとかいってるヤツがいるぞ。
>>108
どんまい
0111１３２人目の素数さん
2005/09/14(水) 22:50:40そうだよ
0113109
2005/09/14(水) 22:57:33有限時間内に真偽を判定することはできませんね。
どうもすいません
0114１３２人目の素数さん
2005/09/14(水) 22:58:33高校数学の本閲覧したけど…１社だけ、JavaScriptだなｗ
確かに、関数型を通り越して、オブジェクト指向言語だわ。
で、こんなの勉強していちいち
<html><head>
<script language="JavaScript">
<!--
スクリプト本体
//-->
</script>
<head>
なんて、訳もわからず入力しているの想像すると…コピペするにして
も、何か非常に可哀想になってくるんですけど。
そりゃ、「極一部」のソフトで飯食おうとするヤツは別だろうけどさあ。大体、
そんなヤツは学校じゃなく自力で覚える！
0115１３２人目の素数さん
2005/09/14(水) 22:59:360116１３２人目の素数さん
2005/09/14(水) 23:03:04r.e.だけだと偽かどうかを判定する手続きが止まらない可能性があるから
そういう意味では真偽を判定出来ないとも言える。
decidable(=recursive)ではないってことだ。
0117１３２人目の素数さん
2005/09/14(水) 23:08:18＞高校数学の本閲覧したけど…１社だけ、JavaScriptだなｗ
マジ？！！
これで勉強させられるヤツら悲惨だな…。
本質的でない部分が多く含まれる上に、どうせ教える側も良くわかってないんだろうし。
0118１３２人目の素数さん
2005/09/14(水) 23:20:28まともな、高校数学教師なら、その教科書のその部分は「飛ばすべき」だ。
後で、校長や教頭から文句がくるやも知れないが、その方が「良心的」だと思う。
0119１３２人目の素数さん
2005/09/15(木) 08:52:32Ｃ言語でLispコンパイラを書けばいいじゃないか。
0120１３２人目の素数さん
2005/09/15(木) 08:55:41コンパイラを書くと何がいいの？
0121１３２人目の素数さん
2005/09/15(木) 09:08:46>「この世のすべての定理」を列挙することは一応できるけど
「この世のすべての定理」って、意味がよくわからない。
現在人類に知られている定理のすべてっていう意味？
因みに、当然だけど、可算無限集合の要素を有限時間内にすべて列挙する
ことは出来ない。
0122１３２人目の素数さん
2005/09/15(木) 09:34:54>人間機械論を否定したゲーデルの論文があると聞いた。
岩波の文庫本だったか啓蒙的な本を読んだだけなので詳しいことは
わからないけど、ゲーデルの趣旨は多分、以下のようなことだろうと
想像する(この想像が間違っていることも大いに有り得る)。
不完全性定理は機械には証明できない。よってそれを証明した
人間(ゲーデル)は機械では有り得ない。
0123１３２人目の素数さん
2005/09/15(木) 10:52:130124１３２人目の素数さん
2005/09/15(木) 10:58:28チューリングマシンのような機械ではないということ。
0125122
2005/09/15(木) 11:50:58>不完全性定理は機械には証明できない
自分で言い出してなんだけど、これ本当かな。
原理的には機械にも可能なような気もするな。
もしそうならゴメン
0126１３２人目の素数さん
2005/09/15(木) 11:51:30ちょっと唐突だけど、ピタゴラス数（ ａ^2 + ｂ^2 = ｃ^2 ) の基本解についてはかなり昔から知られていたよね。
基本解を導く手順のなかに「ｃは奇数である」とか「ａかｂのどちらか一方だけが偶数」なんていうのが現れる。そして最後にいくつでも簡単にピタゴラス数を計算できる方法を導いている。「昔なのにすごいなぁ」などと感心したもんですよハイ。
ピタゴラス数の基本解の導き方は今の中学生でも簡単にできる問題なので、自動証明のプログラムの例題としても比較的簡単そうだし、もしかしたら既に誰かがやっていると思うんだけどなあ。でもニュースなどでこれに近いことすら聞いたことがないのですよハイ。
0127１３２人目の素数さん
2005/09/15(木) 12:32:01その定理に使えそうな命題をいくつか組み合わせて推論し、
それが成功しないときは別の組み合わせを試す。つまり試行錯誤。
組み合わせというより、いろいろな方法と言ったほうがいいかもしれない。
定理によっては証明のパターンというものがある。
この種の定理にはこの方法を使うというような。
だから、問題を解く経験を含めた広い意味の知識というのは大きな要素
であるのは間違いないと思う。
0128１３２人目の素数さん
2005/09/15(木) 13:23:13量子力学的ゆらぎとか。
そのノイズによりひらめきが誘発されるとか。
0129１３２人目の素数さん
2005/09/16(金) 16:56:49>自分で言い出してなんだけど、これ本当かな。
もちろん初歩的な誤り。
不完全性定理は形式的証明が可能。
証明できないのはゲーデル命題。
もっとも、人間にも証明できないわけだが。
0130１３２人目の素数さん
2005/09/16(金) 22:46:54ってことは出来るのかな？
0131１３２人目の素数さん
2005/09/16(金) 23:33:140132１３２人目の素数さん
2005/09/18(日) 04:33:41図は別に使わないだろうけど、補助線の考え方自体は要るよね。
あれは激しくセンスが必要な気がするんだが…。
0133１３２人目の素数さん
2005/09/18(日) 05:48:570134１３２人目の素数さん
2005/09/18(日) 11:17:390135１３２人目の素数さん
2005/09/18(日) 11:57:540136１３２人目の素数さん
2005/09/19(月) 00:33:41適当に総当たりで補助線引いてみて、過去の定理を当てはめることができるか、
総掛かりで検索する…とか。
0137１３２人目の素数さん
2005/09/19(月) 11:58:12家産
0138１３２人目の素数さん
2005/09/19(月) 15:04:55証明の方法まで指定するのか？
コンピューターで計算するんなら、座標やベクトルを使うことになるんじゃないのかな。
0139１３２人目の素数さん
2005/09/21(水) 14:20:02この前提となっているのは、「アルゴリズム」として、
有限長のものをどんな命題にも先立って与えるとしたら、
ということです。
命題を与えられてからそれを観た後であれこれとアルゴリズムを
生成していって、一般には有限個とは限らずに無限のアルゴリズム
列を作っていきながら判定を試みるというやり方であれば、
どうなるのかについては証明法の範囲外であると思います。
（この場合、「アルゴリズム」の列全体は可算ではないのです）
0140１３２人目の素数さん
2005/09/21(水) 15:46:10数学的帰納法で証明できる自然数の定理は、
すべてコンピュータで自動証明できるか？
0141１３２人目の素数さん
2005/09/21(水) 22:05:49ペアノの公理系の帰納法は、自然数の集合あるいは自然数の命題に関する公理。
ペアノ算術の帰納法は、初等的命題に関する公理スキーマであり適用範囲が制限される。
このため人間が数学的帰納法により証明できる自然数の定理であっても、
その証明を一階述語論理＋ペアノ算術で形式化できない可能性がある。
0142１３２人目の素数さん
2005/09/22(木) 08:03:10ペアノの公理系は形式化されたもの。
証明があるなら当然コンピュータで自動証明できる。
しかし証明がない場合には延々と止まらない。
したがって、有限時間で全ての定理を
証明し切ることはできない。
0143１３２人目の素数さん
2005/09/22(木) 15:14:370144１３２人目の素数さん
2005/09/22(木) 18:10:03人間ならできる！といった覚えは一度も無いが
0145１３２人目の素数さん
2005/09/22(木) 21:22:110146１３２人目の素数さん
2005/09/23(金) 05:21:34それは命題を入力として証明手続きを列挙する手続きの存在を仮定してるから
結局同じことなんだが。
あと真でない命題を入力した時に有限時間内に終わらない可能性がある。
最終行の可算は有限の間違い？
0147１３２人目の素数さん
2005/09/23(金) 15:41:29（本当はこういうことはないのだが、N文字で書かれた任意の命題を
証明することのできる・あるいは否定できる手続きのプログラムで
１０＾１０＾N文字以内で書けるものが常に存在する、
というようなことがあったと仮にしてみよう。もちろん嘘だが）
もしもそうであれば、
そのとき、ある任意の命題（その長さをN文字としよう）
が与えられたとして、それから始めて、１０＾１０＾N文字以内の
プログラムをすべて列挙して調べれば原理的には答えがわかる
ということになる。
ところが、全く任意の命題が与えられるとするならこの方法は使えない。
なぜならNが事前には抑えられていないので、予め有限長のプログラムを
用意しておくなどということが出来ないのだ。
つまり、もしも、このような状況であれば、
やってきた入力を観た後からだと可能である。ところが
どんな入力が来ても処理できるように事前に準備することは
出来ない、のである。
0148１３２人目の素数さん
2005/09/29(木) 16:19:50夫馬です。
黒木先生。この基礎論・計算科学屋を叩いて下さい。
「完全証明」という専門用語を使い、「今まで数学
的に完全な証明がなかった！」というように素人に
思い込ませる。コケオドシをやっています。ポモ的
です。やっつけて下さいな。
＞フランスの数学者カミーユ・ジョルダンが１８８７年に概念を確立し、その後多くの
＞数学者らが完全証明に挑んできた「ジョルダンの曲線定理」について、信州大
＞工学部の中村八束（やつか）教授（６２）が２７日、ポーランドの数学者ら１６人との
＞約１４年間にわたる共同作業で、完全証明に成功したと発表した。数式上の誤り
＞などを確認するコンピューターシステムのチェックを経て、約２０万行にわたる証明が
＞完成。中村教授らは「完全証明したのは世界初」としている。
http://www.mainichi-msn.co.jp/shakai/wadai/news/20050928k0000m040137000c.html
0149１３２人目の素数さん
2005/09/29(木) 16:23:20コケオドシだから、黒木にこいつらを叩く資格はないよｗ
0150１３２人目の素数さん
2005/09/29(木) 16:25:11>>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
0151１３２人目の素数さん
2005/11/10(木) 18:44:300152１３２人目の素数さん
2005/11/10(木) 20:55:41ものまでＡとかＢとかいう記号で扱うことに対して、無意識の不安、抵抗
があるからであろう。
これを払拭させるには、まず。「命題はモノではない」ということを
明確に意識させたうえで、「それでも命題は或る意味でモノ扱い出来る」
ということを相当徹底的に理解させることが有効であろう。
尤も、この第２段階で徹底的に抵抗するような人物には、この教育法も
無力であろうが、記号論理学嫌いのほとんどは、第１段階によって、自分
の記号論理学嫌いの原因を明確に意識出来れば、次の第２段階も突破する
であろう。
そうなれば、定理の自動証明の基本構想の概念に到達し易くなるであろう。
このスレッドの話はそのあで始めるのが良いだろう。
0153１３２人目の素数さん
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:340253１３２人目の素数さん
2006/01/15(日) 16:51:590254１３２人目の素数さん
2006/01/16(月) 10:58:00何が目的ですか？
詳しい人、いらっしゃいましたら、
ご回答願います。
私が少し興味を引かれる問題は、
公理系や取り扱う論理式の全体に、
どのような制約を設ければ、
任意に与えられた論理式が証明可能か
不可能かを機械的に判定できる
アルゴリズムを作れるか？
という問題です。
（興味のない人、ごめんなさいね～）
0255１３２人目の素数さん
2006/01/16(月) 11:04:33地球上の人口が増えていくのはどう説明してるんだろう。
0256１３２人目の素数さん
2006/01/16(月) 14:28:11「人は死んだら生まれかわる」と「人はみな、過去に死んだ人の生まれかわりである」が
違うことは理解しているか?
ついでに言っておくと、ゲーデルは来世が未来の地球だとも未来の"この世"だとも
書いてないよ。
0257１３２人目の素数さん
2006/01/16(月) 15:00:40とすると、人間には２種類いることになるのか。
生まれかわりとそうでないもの。
不公平だなｗ
>ついでに言っておくと、ゲーデルは来世が未来の地球だとも未来の"この世"だとも
書いてないよ。
書いてないけど文脈からそうとしか思えない。
0258１３２人目の素数さん
2006/01/16(月) 15:36:540259１３２人目の素数さん
2006/01/16(月) 16:46:25致命的だな。これじゃ生まれ変わりだろうがそうでないだろうが
実質同じこと。
0260１３２人目の素数さん
2006/01/16(月) 18:05:570261１３２人目の素数さん
2006/01/16(月) 22:38:270262１３２人目の素数さん
2006/01/17(火) 09:00:51俺は兄の生まれ変わりなのか
あと、クローン人間禁止されたら俺は殺されるのか
0263１３２人目の素数さん
2006/01/19(木) 03:46:05自然数があるのに命題論理とは・・・。
248の言うとおり、ＲＥだと言っているだけだよ。
いい加減な知識に基づいて考えるのは危険だよ。
0264１３２人目の素数さん
2006/01/22(日) 03:41:20OMOIKOMI NO HAGESHII YATSUYONOO
0265１３２人目の素数さん
2006/01/22(日) 22:57:180266１３２人目の素数さん
2006/01/23(月) 22:48:57仰るとおり。ごめん。２４４は誤り。
0267１３２人目の素数さん
2006/01/24(火) 09:42:340268１３２人目の素数さん
2006/01/29(日) 05:19:47近年再び盛んになった人間の脳の機能や構造の研究であろう。
数学を行う作業を、脳の活動をリアルタイムでモニタリングする
帽子をかぶりながら、知的作業に対して脳が如何に使われるかを研究
するのである。おそらく、代数学と幾何学では使われる部位が
違っているとか、そういう類の発見とか、あるいはある事柄
を抽象化したり一般化したりする脳の機能の解明の糸口が
みつかるかもしれない。さらに、頭蓋を外してここだとめぼしを
つけた部位に電極をさして、。。。。。
そのようにして、脳の推論する機能が段々よく分かってきたら、
あるとき偉大な者が現われて、脳シミュレータを開発し、ついに
プログラムによらない自己学習型、自己発見型、自己推論型の
人工数学者ができるかもしれない。彼は外界の情報をネットと
電子ライブラリーを参照しながら、ただもくもくと数学にいそしむ
のである。世間はこのシステムの完成をみて、もはや数学者は要らない
と短絡的な意見に走り、数学者を野に放って数学以外の労働を
強制するかもしれない….
0269１３２人目の素数さん
2006/02/05(日) 07:27:080270１３２人目の素数さん
2006/03/02(木) 16:59:590271中川泰秀 ◆IvNr9.tOCg
2006/03/13(月) 16:40:570272１３２人目の素数さん
2006/03/14(火) 04:35:180273１３２人目の素数さん
2006/03/14(火) 14:46:41証明しようとすると、必ず自己矛盾か無限ループに落ちるから
考えないようにしている。自己のことを考察した瞬間に
システムのどこかに必ず不動点が生じて、そこで引っかかって
抜けて来れなくなるのだ。
0274中川秀泰 ◆IPeKUwqiHM
2006/03/14(火) 14:50:55これはコンピューターばかりでなく人間にも当てはまる。
0275BW of Tama King
2006/03/14(火) 14:54:52奴は数学の召喚獣スクリプトだから。 普通あんなけレス出来んぞ。
キング無理すんなよー オーバーヒートするぞぉー
0276GiantLeaves ◆6fN.Sojv5w
2006/03/14(火) 15:00:040277BW of Tama King
2006/03/14(火) 15:01:300278中川秀泰 ◆IPeKUwqiHM
2006/03/14(火) 15:07:02等というking見た事無し
0280BW of Tama King
2006/03/14(火) 15:45:120281１３２人目の素数さん
2006/03/26(日) 14:29:190282１３２人目の素数さん
2006/04/04(火) 22:11:130283１３２人目の素数さん
2006/04/15(土) 23:09:200284中川秀泰
2006/05/12(金) 05:31:360285１３２人目の素数さん
2006/05/13(土) 22:25:060286１３２人目の素数さん
2006/05/14(日) 05:01:340287１３２人目の素数さん
2006/05/16(火) 15:42:020288１３２人目の素数さん
2006/05/16(火) 16:04:340289１３２人目の素数さん
2006/05/26(金) 14:14:490290１３２人目の素数さん
2006/06/16(金) 01:05:040291１３２人目の素数さん
2006/07/28(金) 15:37:130292１３２人目の素数さん
2006/08/15(火) 04:09:52あ あ あ ああ あ あ あ
あ あ あ あ あ あ あ
ああ あ あ あ あ あ あああああ
あ あ あ あ あ あ あ あ
あ あ あ あ ああ あああああああ
あ あ あ あ あ あ
あ あ
あ あああああ
あ ああああああ
あ あ ああ あ
あ あ あああ ああああ
あ あ あ あ あ あ
ああああ あ あ
0293KingOfUniverse ◆667la1PjK2
2006/08/17(木) 06:00:12人の脳を読む能力を悪用する奴を潰せ。
0294１３２人目の素数さん
2006/08/30(水) 16:55:540295１３２人目の素数さん
2006/10/03(火) 00:21:380296１３２人目の素数さん
2006/11/12(日) 23:47:290297１３２人目の素数さん
2006/12/07(木) 20:24:250298１３２人目の素数さん
2006/12/07(木) 20:38:28なぜ出来ないか考えるきっかけになる。
0299１３２人目の素数さん
2006/12/07(木) 20:52:470300１３２人目の素数さん
2006/12/07(木) 21:30:46円のあいだの領域に飛ばして、グラフが１に収束する力学系を
つくればいいんでしょ？
0301数学系のD1です
2006/12/07(木) 21:43:09ありがとうです
0302１３２人目の素数さん
2006/12/07(木) 23:13:55は直線を同心円にマッピングする。
0303１３２人目の素数さん
2006/12/07(木) 23:41:34は直線を同心円にマッピングする。
0304１３２人目の素数さん
2006/12/07(木) 23:42:340305１３２人目の素数さん
2007/01/01(月) 00:05:23↓このスレを見ている人はこんなスレも見ています。(ver 0.20)
0306１３２人目の素数さん
2007/02/05(月) 17:08:310307１３２人目の素数さん
2007/02/07(水) 04:18:000308１３２人目の素数さん
2007/02/07(水) 05:05:150309１３２人目の素数さん
2007/02/07(水) 11:50:21最適（に近いもの）を一瞬で見つけられるのはなぜなんだぜ？
0310１３２人目の素数さん
2007/02/07(水) 21:31:580311１３２人目の素数さん
2007/02/08(木) 06:28:03逆もあるよん
0312１３２人目の素数さん
2007/02/10(土) 18:55:120313１３２人目の素数さん
2007/02/11(日) 13:27:430314１３２人目の素数さん
2007/03/11(日) 17:58:470315１３２人目の素数さん
2007/03/15(木) 23:25:07人間も全数探索に近いことをするけど、
コンピュータより早く終わらせられるのは、
その先に答えがあるかどうか評価する能力の違いなんだよ
ゲーム木を育てるジョウロだけじゃなくて、その枝を刈る鋏も重要なんだよ。
ようするに翠s
0316１３２人目の素数さん
2007/03/16(金) 00:59:14有名なんで紹介するのも気が引けるんだけど、Coqっていうソフトやら、証明
を形式的に記述して検証するものっていろいろあるよね。
その手のソフトの下地の理論を探れば、検証する方法の勉強はできそうだが。
0317１３２人目の素数さん
2007/03/16(金) 04:06:48プルーフチェッカのMizarってのをけっこういじったけど、
けっこう面白かった。
ただ言語仕様がどこにもはっきりと書いてなくて、(基本はpdfとかに書いてあった)
既存のライブラリを読んで自分で考えないといけなかった。
なんか基本は述語論理での推論法則だけを使ってやるって感じだったな
でも等式とかの導出を詳細に(両辺からxを引いたとか)書かないでも
成り立っててかつあんまり飛躍してなければ受理されたけど、
そのへんはどうなってるかわからなかった。
論理的にすっきりした証明を選び出せば十分なんじゃないかなー
自動証明は証明可能かどうか、あと数学自体が無矛盾じゃないか、
の判定だけでいいと思う。
0319１３２人目の素数さん
2007/06/24(日) 23:48:150320１３２人目の素数さん
2007/06/25(月) 00:28:07ほとんどの数学理論では、無理。
0321エレガントな解答を求む
2007/06/25(月) 00:40:34heuristics を入れなきゃにっちもさっちもいかない
a! ha!なかんじは少なくともTuring Machineには無理だね
人間の脳を細胞レベル、分子レベル、素粒子レベル、、、で解明
できなければサル真似だよ
0322１３２人目の素数さん
2007/06/25(月) 13:43:13べっ、べつにa=bなんて言ってないわよっ！
ただ、a≠bだったとしたら、
あれがあーなったりこれがこーなったりして
いろいろムジュンするって、それだけなんだからっ！
0323１３２人目の素数さん
2007/06/25(月) 14:19:34漏れは逆だと思う。
会うといつも笑顔で挨拶してはくれるが
二人きりで会おうとするとなぜかはぐらかされる。
だからあの笑顔は好意の証ではない。
0324１３２人目の素数さん
2007/06/25(月) 14:21:35お年をめした准教授が
「ツンデレって、なんやねん？」
ツンドラ気候か？って…
0325１３２人目の素数さん
2007/06/25(月) 14:28:09アニヲタには理解は早いかもしれないが
（アニメを知らない）准教授に説明するには
かえって困難だ
准教授の使っているパソコン（win95)みたいな性格のことですよ
と言っとけ
0326１３２人目の素数さん
2007/06/25(月) 14:31:15それは平野文で「ふみ」と読むんだが。
（実はついさっき知ったｗ）
0327１３２人目の素数さん
2007/06/25(月) 14:35:37ガッキー＝ハルヒ キョン＝マツケン
で「憂鬱」実写映画化って、あれマジで無いのか。
長門＝ホマキ 古泉＝平岡祐太 あたりまで
俺の中ではキャスティングが出来上がってるんだが
みくるが・・・・
0328１３２人目の素数さん
2007/06/25(月) 14:48:33そろそろスレ違いっぽくなってきたな…
お前らアニメ板で語ってくれい
0329１３２人目の素数さん
2007/06/25(月) 15:51:51アイドルヲタのニヨイもしてきたが
0330１３２人目の素数さん
2007/06/25(月) 18:48:120331１３２人目の素数さん
2007/07/01(日) 14:51:58も適用できるのではないだろうか。過去の証明を沢山放り込んで
パターンを学習させることで、未知の命題が試行錯誤により、より良く
解けたりしないかな。
特に、正しい命題の場合には、いってみれば詰め将棋のようなものだから、
どうだか分からない命題よりは易しいのではないだろうか？
0332１３２人目の素数さん
2007/07/01(日) 21:06:280333１３２人目の素数さん
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とかを自動で叩き出す。
証明って今までに出された結果が効率的に使えてないから難しいと思うんだよね。だったらそこはコンピュータにやらせようと。
0337１３２人目の素数さん
2007/07/03(火) 09:20:570338１３２人目の素数さん
2007/07/03(火) 10:13:040339１３２人目の素数さん
2007/07/03(火) 11:00:190340１３２人目の素数さん
2007/07/03(火) 11:10:04ちょっと興味あるんだけど、その「性質」ってどういうデータ構造？
0341１３２人目の素数さん
2007/07/07(土) 06:13:46おもしろそうですね。なるほど、自動証明って、
こういうことを研究するのですか。。
0342math太郎
2007/07/07(土) 06:45:59おれは将棋のプログラム作ったことあるよ。
弱いけどね。。。
結局のところ、探索をどこで打ち切るか？というのは速度の
問題でもあるが、つきつめれば盤面評価関数を
どのように作るかの問題なんだ。
盤面評価関数は、その盤面上の状況に数値を
あてはめて、得点をつけるわけだ。
それで得点の高いほうを選択するわけ。
数学の証明をそのように得点化して評価できるかというと、
多分、無理じゃないかな？
0343１３２人目の素数さん
2007/07/07(土) 08:57:21なるほど。
数学の証明に適用するには、
まだまだハードルが高いんですね。
0344１３２人目の素数さん
2007/07/07(土) 09:00:12探索を途中て打ち切って得られた「証明図」が、
所要の命題に正しい証明を与えているか否かの判定も、
別に必要になりますね。
0345１３２人目の素数さん
2007/07/07(土) 09:05:450346１３２人目の素数さん
2007/07/07(土) 09:07:56証明を探索すると結果が出れば必ず正しいけど、なかなか現実的な時間では終わらない。
そこで結果の正しさをある程度犠牲にして計算量を削減しようと。
0347１３２人目の素数さん
2007/07/07(土) 09:11:48正しい証明図がでるまで探索を続けるのだけれど、
現実問題として、探索を途中で打ち切らなければならない。
そのとき得られた解を、
今度は正しい証明図を与えているかどうかの判定にかける
（ミザールみたいなコンピュータ・プログラムで）
・・・ということかな？
0348346
2007/07/07(土) 10:14:140349１３２人目の素数さん
2007/07/07(土) 13:34:410350１３２人目の素数さん
2007/07/08(日) 11:44:290351１３２人目の素数さん
2007/07/08(日) 22:53:3020 if theorem=true print"QED"
30 next i
0352１３２人目の素数さん
2007/07/09(月) 00:44:430353１３２人目の素数さん
2007/07/09(月) 00:56:16昭和のかほりがした
0354１３２人目の素数さん
2007/07/09(月) 01:07:480355１３２人目の素数さん
2007/07/09(月) 12:17:390356１３２人目の素数さん
2007/07/25(水) 23:07:580357１３２人目の素数さん
2007/08/28(火) 02:29:560358１３２人目の素数さん
2007/09/06(木) 23:34:550359１３２人目の素数さん
2007/10/30(火) 12:31:590360１３２人目の素数さん
2007/12/20(木) 09:07:39実用化すれば、レフリー要らなくなるよね
0361１３２人目の素数さん
2007/12/20(木) 15:10:56チェッカに渡す証明を書く手間考えるとやる気にならない
0362１３２人目の素数さん
2007/12/20(木) 15:46:560363１３２人目の素数さん
2007/12/20(木) 16:55:29お前さんは
メールを打つのが、手間かかるので
そのまま、電話をするタイプ？
0364１３２人目の素数さん
2007/12/20(木) 23:39:35いや、電話はなんとなく嫌いなのでメールする
0365１３２人目の素数さん
2007/12/21(金) 13:25:21貧乳だな
0366貧乳はステータスだ希少価値だ
2007/12/22(土) 05:38:17_x≦メ_,-､ ,ｨ≦:_:.／:/ ;ｲi: : :j : : : :＼ {ヽ.__>､_ゝ
. ﾍﾆ ,ｨ r＜ ／:/:/:/ {:| : ∧ : ヽヽﾊ r―-､ ﾉ-ｧ.勹
／ィヽ| ﾄ'ノ / /.:| :{/＼ﾄ: :｣／Vﾊ:', } } ,ｱ / ｢`こﾍ
｀7_} /,イ: :| ﾊｚ== ヽ{ =弍 | |:| | ＜_へ＞ { ｆ=} }_
,-､_fﾍxー､ |: ∧ { ｰ'ｰ' ･}:jﾊ{:.′ __ﾍﾆｱ‐vｨｱﾄ､ヽ-'
. {／ヽﾉｲ¨ｰ' Ⅵ/: i＞ ､ _, ﾘ}│{ ﾍーｧ f ¨くtfｲ |
ｨ_／ |: :|/:.,ｨ=厂{≧': /:∨ /／ r=} ﾄ {__,ﾄ､
／}fﾆニﾍ |: :|ﾍ {¨7´ /: /＼:{ {ﾍ ＜八_＿ ﾉ
≦ｨくﾄrｆ}f,勹 rﾍ: |∧ |/, イ :/ ⌒} |_.} f{ ｨ=士ゝ
. |_}ﾍ-'¨ｰ' 人.ヽ{⌒{7＞.Ⅳ∧ /¨＞ 、ノ＾ﾆ勹 ヾ (f_ﾉｰ､
／}ｰ士= .ヘ `∧, 小、__} / : ｰｧ' ,ノ フ／ ´¨
≦ｨく }`{z} ＼ Ｙ_./ / { ∨:/´ ｨ く ｰｆﾆ勹
. |_}くニニﾍ / ヽ/∨}／｢￣{ｱ:ー' : : ﾍ ／,＜...
r-ﾉ7_ __{ヾ> ｰ≦.ｨ７/ /│ V ﾊﾍ : : : : : : ',≦ｆL ___fヾ>
ﾌ / ,ｲｰ'¨ く/// / :| ∨ﾊ ',: : : ｊ: : :ﾊ ｧ/ ｲｰ'¨´
{./ ゞこﾌ /// / | ∨ﾊﾊ: : :}Ｖ:}: |ﾑ{ ゞこﾌ
//7={...__ | __ ...},ｘ≦: :ﾉ |ﾉⅤ
0367１３２人目の素数さん
2008/01/17(木) 01:09:39個人的には量子論的な乱数の存在がゲーデルさん的な「人間はコンピュータよりつおい」の根源的原因かもと思うのさ。
でさ、時刻とかカーソルの動きとか様々な外部要因を取込んで強化したぎじ乱数を、ぎじでもいいから使うべきだと思う。
既に与えてある定理の一部の文字をランダムに取換とか改変し、その文が論理的に正しい文になるまで取換や改変、を続けさせるとか。
与えられた語彙の中からランダムに定義行為や公理設定行為を行わせてみるとか。
0368367
2008/01/17(木) 01:12:35膨大な汚い小定理や汚い定義の中から、他の小定理や定義からの引用回数が多い程優先度を上げて処理し、
つまり母定理母定義、ハブ定理ハブ定義として進化論的に自然淘汰させるとか。googleみたいな。そこで「ネットワーク理論」とか応用してみたり。
つまり、貧乳は本人が気にしているのも含めて良いのやから誇られたらぐんにょりやね、に一票。
0369１３２人目の素数さん
2008/01/17(木) 01:21:390370367
2008/01/17(木) 01:51:40人間が定理や定義の「善」をコンピュータにいちいち正すのは面倒。
というワケで～進化論的に目指させればそれなりにそこそこの結果でるんじゃないカナ～と思う。なるべく簡潔で汎用性の高いのが生き残ってゆくとかさ。
人間の理性的処理能力だってもともとは遺伝子のコピーミスというぎじ乱数から出たっぽいしさ。
0371１３２人目の素数さん
2008/01/18(金) 09:14:20自動証明したいの？数学の定理生成をしたいの？
新たな数学体系の構築をしたいの？
0372１３２人目の素数さん
2008/01/19(土) 00:02:37ヒント【ゲーデルの不完全性定理】
0373１３２人目の素数さん
2008/01/19(土) 00:10:02不完全性定理がどうしたって？
0374１３２人目の素数さん
2008/01/24(木) 22:52:06その方針だと計算の効率とかには影響を与えるだろうから、
効率のいい（擬似）自動証明方法とかは思いついてくれるかもしれないが、
>>367で書いてるゲーデル的な意味での性能は一つも変わらない。
というか、ちゃんと勉強すれば簡単に分かることなんだけど、
例に挙げているような擬似乱数の類では
コンピュータの計算可能性そのものに関しては何も影響を及ぼさないぞ。
せいぜい計算量レベルの影響しかない。
0375１３２人目の素数さん
2008/03/28(金) 03:47:220376１３２人目の素数さん
2008/05/05(月) 22:47:320377１３２人目の素数さん
2008/05/09(金) 08:29:491. 俺が書いた証明をチェックしたい → Proof Checker (Mizar)
2. 定理をあたえたら全自動で証明を返してほしい → Automatical Theorem Prover (Djinn, Mathematica)
3. 半自動で証明を手伝ってほしい → Proof Assistant (Coq, Isabell)
ただし、2.は扱える領域が極めて狭いので注意!! そして、証明できないときもある。
1.3.はすべての数学的命題を扱うことができるが、人間の努力も必要である。
0378１３２人目の素数さん
2008/05/10(土) 08:06:540379１３２人目の素数さん
2008/05/10(土) 08:43:132は、証明できない場合、フリーズしちゃうんですか？
0380１３２人目の素数さん
2008/05/10(土) 10:39:58証明器によると思う。よく知らない。
ただ、計算量は指数的に膨れ上がる事が知られており、自動証明可能なものであっても、
現実的な時間内には終わらないこともある。
そもそも、自動証明では記述できる命題が限られるため、証明支援器 (377の3.)を用いて、
部分的に自動化する方法が最も現実的である。
0381１３２人目の素数さん
2008/05/10(土) 11:46:39ありがとう。
0382１３２人目の素数さん
2008/05/14(水) 02:44:560383１３２人目の素数さん
2008/05/14(水) 02:48:160384１３２人目の素数さん
2008/05/14(水) 03:44:52つまらん！
１０００までやりゃいいのに
0385１３２人目の素数さん
2008/05/14(水) 10:30:250386１３２人目の素数さん
2008/05/14(水) 11:37:11つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
0387１３２人目の素数さん
2008/05/14(水) 11:38:58つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
0388１３２人目の素数さん
2008/05/14(水) 11:39:28つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
0389１３２人目の素数さん
2008/05/14(水) 11:42:13つまらん！
１０００までやりゃいいのに
ん？タン虫は２連で終わり？
つまらん！
１０００までやりゃいいのに
0390１３２人目の素数さん
2008/05/14(水) 11:47:46いくじなし＾＾
１０００までやんねぇのかYO？
いくじなし＾＾
0391１３２人目の素数さん
2008/05/14(水) 19:49:320392１３２人目の素数さん
2008/05/15(木) 21:42:44> ＞証明可能かどうか、数学自体の無矛盾の判定
> ほとんどの数学理論では、無理。
無矛盾性の証明が無理なのでは無く、無矛盾な公理系の上での
すべての真な命題の証明が無理なのでは。
0393１３２人目の素数さん
2008/05/15(木) 23:37:58有ったのだが、この頃は、Frege構造というものについて気に
なってきたのだよ。フレーゲ構造って、なんか面白そうな予感
がする。
0394１３２人目の素数さん
2008/05/16(金) 07:34:11フレーゲってよく知らないけど、普通のhigher order logicと何が違うの？
0395１３２人目の素数さん
2008/05/27(火) 22:29:390396１３２人目の素数さん
2008/05/28(水) 07:16:42ttp://citeseer.ist.psu.edu/519604.html
0397１３２人目の素数さん
2008/06/28(土) 17:11:46ttp://d.hatena.ne.jp/yoriyuki/20080627
0398１３２人目の素数さん
2008/07/05(土) 10:44:380399１３２人目の素数さん
2008/07/29(火) 11:26:01みたいんだけど、個人的に遊べるソフトはどれがお勧めですか？
今、MIZARとか言うのを解読中なんですが、HIDDEN.VOCが見当たらないんだよねえ。関数記号とかも
自分で定義したいんだけど、そういうのはＭＩＺＡＲには向いてないのかなあ。
もっとグラフィカルでわかりやすいのがあるといいなあ。
0401１３２人目の素数さん
2008/08/01(金) 08:48:26それより、そのノートを公開すれば、いろんな人が各ツールで実装してくれんじゃね？
それをグラフィカルに眺めればok
0402１３２人目の素数さん
2008/08/19(火) 07:41:450403１３２人目の素数さん
2008/08/26(火) 04:40:30「ほとんど全ての命題を自動証明することは出来ない」を意味しない。
もしかすると、
「ごく一部の命題（測度０笑）を自動証明することは出来ない」なのかも
しれない。
また、「正しいと証明できる命題であっても自動証明することは出来ない」
を意味しないことに注意。
ある一つのパターンの命題（証明不能の証明に出てきたようなタイプの
命題）だけが、証明不可能であるだけなのかもしれないのだ。
0404１３２人目の素数さん
2008/08/26(火) 15:11:170405１３２人目の素数さん
2008/08/27(水) 05:35:12補助線引いていくだけだったりするし
0406１３２人目の素数さん
2008/08/27(水) 13:47:02無理でしょうな。平面幾何の定理は非常に多くあるし、その証明は難しい。
よって機械的に証明を探索しても計算量が爆発してオワリ。
0407１３２人目の素数さん
2008/09/03(水) 15:25:07あれって、過去に出された（既出）な問題ってのもあるのかな？ってふと思った
とあるマニアな人間が、過去（１世紀以上も）の詰将棋問題を
データーベースみたいなものに、インプットしてて
例えば今週出題された、詰将棋問題を、そのデーターベースで"検索"したら
ヒットして、19xx年xx月xx日 読＠新聞 にて、同問題がありました とかね
ｳﾝ十年前のNHKで、将棋の特番だったかうろ覚えだが
詰将棋などではなく、実際の戦いの局面の配置を、コンピュータでインプットして"検索"し
同局面が、過去に3度ありました。と出て、先手後手どちらがその後有利または勝ち負けなのかなどの
判定らしきものが、あった。
0408１３２人目の素数さん
2008/09/03(水) 15:44:56たぶん数年前の順位戦A級最終日の中継で勝又5段（当時）がデータベース使ってたときの事だと思うけど
0409407
2008/09/03(水) 16:29:55ウン十年前ではなくて、十ｳﾝ年前か
羽生さんが、全盛期の頃
（今でも、健在ですが・・・）
これと似たようなもんでさ
高校教諭が相加相乗平均に新証明法
http://www.asahi.com/science/update/0816/OSK200808160004.html
この相加相乗平均の証明方法は５０以上あると
それらをデーターベース化して、証明の"判定"みたいなものを作れないかな？
「この証明方法に気づいた人はこれまでにもいたはず。
簡単すぎるので発表済みと思ったのかもしれない」
既出な証明であった or 新証明である とかね
そしてこのような判定プログラムを一般人の人でも、扱えるシステムを設けるとかね
0410１３２人目の素数さん
2008/09/03(水) 16:40:00A SIMPLE PROOF OF THE GEOMETRIC-ARITHMETIC MEAN INEQUALITY
http://www.emis.ams.org/journals/JIPAM/images/080_08_JIPAM/080_08_www.pdf
0411１３２人目の素数さん
2008/09/06(土) 23:35:120412１３２人目の素数さん
2008/09/17(水) 09:30:27遅レスですが「詰め将棋データベース」はもちろん存在します。
但し、有償でかなり高価なものらしく（セット全体で10万円くらい？）
Web上などで誰もが検索や同不同チェックができるようにはなっていないようです。
0413１３２人目の素数さん
2008/09/17(水) 12:08:18参考になりました。ありがとうございます。
詰め将棋データベースの同局面検索機能みたいな感じで
それを数学に使えないかなってね。
例えば、大学入試問題。
大学側が、いろいろ問題を考えて作る。
しかし過去にどこかの大学で似たような問題（または、全く同じ問題）があったらマズイよね
そのような検索機能があったら便利かなってね。
実際は、人間たち（教授・准教授その他）が、案外手作業で探っているのかもしれないｗ
過去問題集（赤本）とか引っ張り出してね。
事実、国語の分野では、煮詰まっているらしく
過去の問題を使いまわしを認めるかどうか検討しているらしい
（それは、著作権などの問題があるので、円滑には進まないとか）
0414１３２人目の素数さん
2008/09/18(木) 00:41:410415１３２人目の素数さん
2008/09/18(木) 13:38:210416１３２人目の素数さん
2008/09/18(木) 14:48:130417１３２人目の素数さん
2008/09/18(木) 21:40:13アルゴリズムうｐ
0418１３２人目の素数さん
2008/09/29(月) 11:11:26その言語で数学の論文書くと証明をチェックしてくれるんだってさ。
いまそれでチェック済みの論文がデータベース化されていて、
そこで既に証明済みの定理も新しい定理の証明に使用できてそれをまたチェックできるんだって。
ttp://www.cs.ru.nl/~freek/mizar/
ただしその言語での論文は通常の4倍くらいの長さになるそうな。
0419１３２人目の素数さん
2008/09/29(月) 11:58:17Mizar自体は激概ではあるが、しかし僅か4倍で済むというのは意外だった。
0420１３２人目の素数さん
2008/09/30(火) 06:14:42労力的に絶対無理だから考えるだけ無駄か
0421１３２人目の素数さん
2008/10/16(木) 18:06:180422１３２人目の素数さん
2008/10/25(土) 15:20:260423１３２人目の素数さん
2008/10/28(火) 09:26:13数学はゲーデルの不完全性定理により真でも偽でもない命題がある。
だからコンピュータと数学は合わない。
真でも偽でもない命題をコンピュータにやらせたら
無限ループに陥る。
その場合は
if p<>true and p<>false then
exit sub
endif
と書くといい。
0424１３２人目の素数さん
2008/10/28(火) 20:26:040425１３２人目の素数さん
2008/11/03(月) 12:00:340426１３２人目の素数さん
2008/11/03(月) 12:16:34すべてのパターンを実行しても反例が見つからなければ証明されたと言える
無限の場合は無理
0427１３２人目の素数さん
2008/11/03(月) 21:11:320428１３２人目の素数さん
2008/11/03(月) 21:40:240429１３２人目の素数さん
2008/11/10(月) 21:06:19紛らわしい名前のソフトがあった
0430１３２人目の素数さん
2008/12/03(水) 16:40:180431１３２人目の素数さん
2009/01/03(土) 09:07:39そんなわけねーだろ
0432１３２人目の素数さん
2009/01/03(土) 18:49:58どっちかといえばシュミレーション板やプログラム板になるのかな
でも理論的なことを語るのに数学板にも一つぐらいあってもいいと思うんだが
0433１３２人目の素数さん
2009/01/09(金) 15:19:33シュミレーション？？？
大丈夫ですか？
0434１３２人目の素数さん
2009/01/09(金) 15:57:52○確率
×確立
○置換
×痴漢
○偏微分
×変微分
○整式
×正式
○小数
×少数
○有理化
×有利化
○対数
×大数
（ただし『大学への数学』または"大数の法則"の意の場合も・・・）
○シミュレーション
×シュミレーション
（日本語にない発音のため。ただし方言には近い発音があるらしい）
○キチ（既知）
×ガイチ
（またちなみに、既出（きしゅつ）と読む。"がいしゅつ"ではない。）
0435１３２人目の素数さん
2009/01/10(土) 11:21:38×加算無限
○最大元
×最大限
○単項イデアル整域
×炭鉱胃である聖域
0436１３２人目の素数さん
2009/01/11(日) 02:38:33一番下ねえよｗｗｗｗｗｗｗ
0437１３２人目の素数さん
2009/01/11(日) 23:19:48o 正則行列
x 生息行列
o 単射である
x 単車である
o 閉包を得る
x 兵法を得る
0438１３２人目の素数さん
2009/01/12(月) 05:45:54無理だろ。
そもそもC言語もVBもmathematicaも、√2の計算すら
どうせどっかで四捨五入してるんだろ？
じゃないと永久に表示できないからな。
定理の証明に四捨五入なんてしたことないぞ、おれは。
0439１３２人目の素数さん
2009/01/12(月) 13:57:56なんでコンピュータがわざわざ四捨五入とかいう十進法に依存した方法を使わなならんのだ
0440１３２人目の素数さん
2009/01/12(月) 14:10:410441１３２人目の素数さん
2009/01/12(月) 16:12:02大して知らないのに、知ったかすると恥ずかしいよ。
0442１３２人目の素数さん
2009/01/12(月) 19:09:39なら答えてもらおうか。
√2の計算は四捨五入するかしないか。
定理の証明において四捨五入するかしないか。
0443１３２人目の素数さん
2009/01/12(月) 19:19:370444１３２人目の素数さん
2009/01/12(月) 20:40:210445１３２人目の素数さん
2009/01/12(月) 21:09:570446１３２人目の素数さん
2009/01/12(月) 21:17:40実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、
証明に使う性質は、「x^2-2=0 の根である」という代数的性質から全て導かれる。
まあ、実際、代数学の証明の幾つかは既にコンピュータに載せられているものもあるし
人間が既にやった数学的証明は、コンピュータに載せることは可能。
ただし、コンピュータが人間の解いてない数学の定理を証明するような
自動証明ができるかどうかとなると話は別だが。
0447１３２人目の素数さん
2009/01/12(月) 23:56:08>実際、数学の証明を書く場合にも、その正確な値を書くことなんてしないし、
例えばC言語は10桁目で四捨五入するようになっていると仮定する。
√ｘと√ｙは18桁目までは同じで、19桁目から違う数になるとする。
するとC言語では√ｘ＝＝√ｙとなってしまう。
√○を記号として扱おうがこれは避けることの出来ないものだ。
するとC言語では実数の大小関係が確定できないことになる。
大小関係が確定できないということは、実数における命題のほとんど全ては
証明することができないことになる。
0448１３２人目の素数さん
2009/01/13(火) 00:02:17if(x=!y)
{
while(√ｘ＝＝√ｙ）
{
√ｘの小数点以下を求める処理
√ｙの小数点以下を求める処理
}
}
というわけで>>447は取消ということで。
しかし、コンピューターで証明というのは無理だと思うね。おれは。
0449１３２人目の素数さん
2009/01/13(火) 00:08:35計算機での証明を行う場合も、四捨五入なんかする必要はない
>>446のように何らかの代数的性質を満たす記号として √ を導入すればいいだけ
√x と √y の大小関係もその代数的性質から証明できる話。
>>448のやり方がそのひとつだな
まあ、コンピュータによる完全な自動証明は無理だが、
人間がやる証明の支援くらいは出来るようになるかもしれないとは思っている
0450１３２人目の素数さん
2009/01/13(火) 00:12:51一応コンピュータでの証明支援は既にあることはある。
0451１３２人目の素数さん
2009/01/13(火) 11:11:080452１３２人目の素数さん
2009/01/14(水) 10:26:500453１３２人目の素数さん
2009/01/14(水) 10:58:01ver4から3次元曲面がマウスでぐりぐりできるようになったよね。
0454１３２人目の素数さん
2009/01/14(水) 12:32:490455１３２人目の素数さん
2009/01/15(木) 10:05:39あらゆる実数に関する命題は
具体的数値（1,2,3,4,5,6,7,8,9,0）を全く使用せず
抽象的数値（a,b,cなど）で全て証明することができる。
という定理があるということか？
0456１３２人目の素数さん
2009/01/15(木) 10:09:400457１３２人目の素数さん
2009/01/15(木) 10:28:410458１３２人目の素数さん
2009/01/15(木) 10:30:090459１３２人目の素数さん
2009/01/15(木) 10:58:22長々と説明なんてしなくていい
そういう定理が「ある」か「ない」か
2文字で済む話じゃないか。
0460１３２人目の素数さん
2009/01/15(木) 12:47:08√2を小数で表した物が具体的数値で√2が抽象的数値だって？
誰の脳内設定だよ 実数の構成も理解して無いだろ
0461１３２人目の素数さん
2009/01/15(木) 13:12:280462１３２人目の素数さん
2009/01/15(木) 14:36:30＞そういう定理が「ある」か「ない」か
に答えてもらえば解決すると思ってんだからなあ。マナカナのどっちが美人かを決めれば
解決すると思い込むのと変わらんよなあ。
結局、バカは自分がバカだと認識することはできないんだなあ。
0463１３２人目の素数さん
2009/01/15(木) 15:05:45晒しあげ
0464１３２人目の素数さん
2009/01/15(木) 15:12:310465１３２人目の素数さん
2009/01/15(木) 16:51:59そんな長い文章はいらない。2文字でいい。
>>464
実数に関する証明はあらゆるをつけなければ意味がない。
たった２，３個の実数で成り立った所で何の意味もない。
∀a∈Rについて成り立たなければそれは実数における定理の資格はない。
抽象的な文字（a,b,c・・・）で解決できるから
具体的な数値など求める必要はないと言ったのはそっちだ。
そういう定理がなければそんな発言は出てくるはずがないからな。
0466１３２人目の素数さん
2009/01/15(木) 16:53:40どっちが晒しあげられてるかも気付かないのね・・・
0467１３２人目の素数さん
2009/01/15(木) 16:59:32「ない」
というか具体的数値とやらを使用しようがしまいが
あらゆる実数に関する命題を全て証明することはできない
0468１３２人目の素数さん
2009/01/15(木) 17:02:32晒しあげ
0469１３２人目の素数さん
2009/01/15(木) 17:03:530470１３２人目の素数さん
2009/01/15(木) 17:07:27Mathematicaで「√3＞√2」を評価したとき
それぞれを小数展開してそれらの各桁を比べてるとでもと思ってるの？
0471１３２人目の素数さん
2009/01/15(木) 17:19:29ではでは。
0472１３２人目の素数さん
2009/01/15(木) 17:22:160473１３２人目の素数さん
2009/01/15(木) 17:24:28＞あらゆる実数に関する命題は
は
あらゆる実数に関する「証明済みの」命題は
ってことね。
0474１３２人目の素数さん
2009/01/15(木) 17:27:01本当に知りたいなら付き合う気はあるけど
言葉遊びがしたいだけなら流石にやる気は無いぞ
0475１３２人目の素数さん
2009/01/15(木) 17:43:110476１３２人目の素数さん
2009/01/15(木) 17:53:34超数学的なことをせずスピードを問わないのならどうとでもなる
0477１３２人目の素数さん
2009/01/15(木) 20:25:350478１３２人目の素数さん
2009/01/16(金) 01:51:07真実追求しかしていない。
抽象的数値a,bには大小関係が定義されていない。
aとbどっちが大きいか？という問いに意味がない。
アルファベットに大きいも小さいもないからな。
a、bに具体的数値を代入して初めて大小関係が定まる。
ところが、ここの住人は具体的数値を求める必要はないと言う。
じゃあ質問するがaとbはどっちが大きい？
ただしaとbには具体的数値は代入されていないものとする。
ただ、おれは>>448で大小関係はプログラムで求められることに気づき
その部分においてのみ、自らのあやまちは認めたはずだ。
0479１３２人目の素数さん
2009/01/16(金) 02:27:10晒しあげ
0480１３２人目の素数さん
2009/01/16(金) 06:17:04どのレスだよ
0481１３２人目の素数さん
2009/01/16(金) 12:16:160482１３２人目の素数さん
2009/01/16(金) 19:26:59a^2=xを満たす正の実数aと、b^2=yを満たす正の実数bがともに存在するとしよう。
このとき、a≧bと仮定すると、x=a^2≧b^2=yとなり矛盾する。
従ってそのようなa,bが存在すれば、a＜bである。
0483１３２人目の素数さん
2009/01/16(金) 22:13:330484１３２人目の素数さん
2009/01/17(土) 02:27:00この時点でダメだな。
単なる文字に大小関係は無いの。
ｘ＜ｙとする
なんてやってるということはｘとｙにはなんらかの実数、
つまり具体的数値が代入されていることを予定しているんだろ？
アルファベットに大小関係は無いの。
もうほっとこう。だめだ。
0485１３２人目の素数さん
2009/01/17(土) 02:42:12（´,_ゝ｀）ﾌﾟｯ
0486１３２人目の素数さん
2009/01/17(土) 03:18:41吠えてるスレはここですか？
0487１３２人目の素数さん
2009/01/17(土) 07:58:27晒しあげ
0488１３２人目の素数さん
2009/01/17(土) 21:16:41内燃機関を発明できるか？
どういう構造にしたら効率がよいか、とかは得意だろうけど
仮にできたとして、
内燃機関を発明するアルゴリズムは、内燃機関を知っている何かでなければ構築できないのではないか？
0489１３２人目の素数さん
2009/01/17(土) 22:05:18実際に打つ前にフローチャート書く。
（フローチャートを書かなくても、図とか絵とか描いて矢印書いたりして
なんらかのフローチャートもどきは書く）
ならそのフローチャートが証明になっちゃってるじゃん。
0490１３２人目の素数さん
2009/01/17(土) 22:33:28自動証明ってのは、プログラムを生成するプログラムを書くような
ものなんだよ。
0491１３２人目の素数さん
2009/01/17(土) 23:36:28そのプログラムはフローチャートでは表すことは出来ないの？
0492１３２人目の素数さん
2009/01/17(土) 23:48:14知ってていってんだろうな。
つーか。ゲーデル数化も何もしらなそうだな。
0493１３２人目の素数さん
2009/01/17(土) 23:51:30↑教えてください！
0494１３２人目の素数さん
2009/01/17(土) 23:53:40アルゴリズムって言うとき、自分の感覚では、証明出来るなら証明し、出来ないなら出来ないと有限ステップでわかるようなものってイメージなんだけど。
0495１３２人目の素数さん
2009/01/18(日) 00:09:54マルチ
0496１３２人目の素数さん
2009/01/18(日) 03:16:45その定理が真であることを求めるプログラムをCでも何でもいいんで
書いてもらえませんか？
ピタゴラスの定理でもいいですよ。
0497１３２人目の素数さん
2009/01/18(日) 10:41:50いやいや、すまんかった。結局こういうやつ>>496がいるからさあ。ちったあ入門くらい自分でやれ
と言いたくなる。
0498492=497
2009/01/18(日) 10:46:57少しはヒント出すか。１，２，３，．．．と自然数を順に調べていけば、その中にピタゴラスの定理の証明が
あるんだけど。意味わかんねーだろ。だから、ゲーデル数化ぐらい知っとけっての。
あ、それから、真であることを求めるプログラムじゃなくて、証明を見つけるプログラムな。
真と証明可能の違いくらいも早く知っとけ。
0499１３２人目の素数さん
2009/01/18(日) 11:18:47うん、わかんね。
真と証明可能の違いはわかる。
真だからといって証明可能かどうかは保障されてないもんな。
でも証明可能なら真ってことだ。
0500１３２人目の素数さん
2009/01/18(日) 11:20:15だいたいでいいんだけどさ。
500行ぐらい？
それとも100億行ぐらい？
0501１３２人目の素数さん
2009/01/18(日) 11:22:59日本語で？
0502１３２人目の素数さん
2009/01/18(日) 12:41:55ヒルベルトのプログラムだのゲーテル数だのを持ち出す方が
よっぽどバカだと思うのだが．．．。
そういう無茶な風呂敷の広げ方をするから、
一般人は>>500のような反応をするわけで。
実際に自動証明の研究でやっていることはといえば、特定の分野で
限られた定理の組合せで証明できる範囲に限定して、
前提となる事実・帰結・推論規則としての定理・定理を適用する上でのノウハウ
等を、その範囲に限定して設計された記述言語で記述しておいて、
それらを利用して、人間には比較的簡単に行えるような証明を構築するプロセスを
計算機にトレースさせるというような試み。
つまり、人間にできないような証明を計算機にやらせるなんてことを
いきなり目指してるのではなく、まずは人間の思考というものを
プログラムでモデル化してみることで、人間的な有機的な物事の捉え方を
計算機で応用するための知見が得られないかを探る基礎的な研究であって
本質的には人間工学に近い分野。あとはノレッジベースとかＡＩ（死語）とか。
実際に素材としている数学の分野は、簡単な定理の組合せで証明できる
初等幾何が主流。それも、ピタゴラスの定理のように数値の計算が
からむようなものは「簡単な定理」の範囲に入らない。
0503１３２人目の素数さん
2009/01/18(日) 16:46:54ゲーテル持ち出しても何の意味もない
0504１３２人目の素数さん
2009/01/18(日) 17:20:16有限ステップでは証明できないが、証明可能な命題ってあるの？
0505１３２人目の素数さん
2009/01/18(日) 20:43:140506498
2009/01/18(日) 21:48:08をを！すまんかった。今は反省している。どうも>>498を読んだときバカにされた気が
して感情的になってしまったようだ。
おわびに、ゲーデル数化をしても、定理の自動証明にはあまり実用的でないということ
を例えで説明しよう。まず、使用する文字を決める。例えば、ひらがな全てでも良い。
カタカナを含めてもよい。いずれにしても使う文字は有限個に決める。例えばN個だと
しよう。文字を2つだけ並べた文字列は有限個しかない。今の例ならN×N個だ。文字を
3つだけ並べた文字列も有限個。4つ並べても有限個。．．．と行くと、いずれは例えば
ふるいけやかわずとびこむみずのおと
というような文字列も現れるし、ピタゴラスの定理の証明として読める文章も現れる。
それに、以上の手続きは簡単なアルゴリズムで書ける。もっと詳しく論理式とか、証明
を定義すれば、任意の文字列に対して、それが何らかの定理の証明になっているかを
判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
あるかどうかの判定をするアルゴリズムも書ける。
0507498
2009/01/18(日) 21:49:45だからといって、以上の方法が実用的でないということは容易にわかると思う。現在の
コンピューターでは演算速度も記憶容量も足りなすぎる。もちろんいずれ以上のような
方法でも十分実用になるような性能を持ったコンピューターが現れる日が来るかもしれ
ないが、そのころにはの方法で、もっと効率よく定理を証明するアルゴリズムが開発さ
れているかもしれない。
長文すまんかった。失礼。
0508498
2009/01/18(日) 21:52:04実用的でないということ。
0509１３２人目の素数さん
2009/01/19(月) 02:29:07なるほど。その発想はなかったわ。
行間を読む行為もしなくて済むだろうし。
要するに定理の証明とは「有限個の文字の羅列」なんだね。
でも、ここで数学をかじってる人間はすぐに一般化したくなると思うんだ。
「無限個の文字の羅列」で表される定理の証明はあるんだろうかとか
「文字と文字の間にじつはさらに文字があるみたいな、実数の稠密性みたいな文字集合」とか。
ところで
数学の定理は有限個の文字で証明できる
という定理はあるの？
0510１３２人目の素数さん
2009/01/19(月) 02:32:060511１３２人目の素数さん
2009/01/19(月) 02:33:510512１３２人目の素数さん
2009/01/19(月) 03:03:500513１３２人目の素数さん
2009/01/19(月) 11:10:46文字数が確定していないんだから
文章の数は無限個だから証明の文章はできないんじゃないの？
ある定理は100文字で証明終わりになるとはじめからわかっているなら
100個の文字のあらゆる組み合わせを調べつくせば済むけど
その定理の証明が100文字で終わることをどうやって事前に知るの？
0514１３２人目の素数さん
2009/01/19(月) 11:11:49>>498が話してるような方面の基礎論は関係なしで
0515１３２人目の素数さん
2009/01/19(月) 11:26:46あ.いうえおか
か.なにぬね
こういう文字集合を定義したら
証明できる命題は増えるんでしょうか？
0516１３２人目の素数さん
2009/01/19(月) 12:09:49ω規則ってどんなのですか？
0517１３２人目の素数さん
2009/01/19(月) 12:57:53科学が信仰する事実そのものという観念は、宗教、特にキリスト教の神観念に近い。
これは科学が西洋社会を起源にもつ文化現象であるという一つの証拠である。
キリスト教の神観念は、人間の外にある絶対者であり、人間にとって認識不可能かつ到達不可能な存在である。
これは正しく科学が前提とする事実そのものの存在と同じである。
ちみなに、仏教では一切の存在に仏の生命が宿ると考える。
仏性=真理は外にある絶対のものではなく、個々の存在に宿る内面的なものである。
真理は自身のうちにあり、外にはないと考える。
科学は真理を人間の意識の外に求めようとする点において、極めてキリスト教的、西洋的である。
到達不可能な絶対者を立てる科学は、キリスト教と同型の思考形態をもつ。
真理そのものがはなから自己のうちに宿ると考える仏教的発想によって、科学は相対化されるのである。
また、構造構成主義もシステム論も、意識から隔絶した事実そのものを定立することなく、世界を記述するので、科学とは観察方法が根本的に異なることになる。
0518１３２人目の素数さん
2009/01/19(月) 17:34:350519１３２人目の素数さん
2009/01/19(月) 18:18:180520１３２人目の素数さん
2009/01/20(火) 02:29:24文字に大小関係を導入したとたんに逃げるか。
おれだよ、おれ。
文字に連続性を持たせたとたんに口を閉ざすか。
もっとさらし上げろよ。
0521１３２人目の素数さん
2009/01/20(火) 10:45:360522１３２人目の素数さん
2009/01/22(木) 03:03:35だから使う文字を有限個にしたところで
出来上がる文章は無限個だろ。
そんなロジックもわからないのか。
あ
ああああ
ああああああああ
ああああああああああああああ
わかるよな？
あだけで無限個文章があるよな？
まさか逃げはしないよな？
0523１３２人目の素数さん
2009/01/22(木) 04:04:150524１３２人目の素数さん
2009/01/22(木) 20:00:18グッドスタインの定理を途中に出てくる式全部きっちり計算して証明すればいいし
チャイティンの定数も十進表記で計算し終わってから議論すればいい
0525１３２人目の素数さん
2009/01/23(金) 02:11:290526１３２人目の素数さん
2009/01/23(金) 05:55:360527１３２人目の素数さん
2009/01/23(金) 14:16:25晒しあげ
0528１３２人目の素数さん
2009/01/24(土) 01:52:30よく戻ってきたな。
じゃあ話を聞かせてくれ。
ゆっくりでいいぞ。
緊張しなくていいんだぞ。
0529１３２人目の素数さん
2009/01/24(土) 05:05:11晒しあげ
0530１３２人目の素数さん
2009/01/24(土) 09:49:08,,==≡ミヽミヾミミミ、ヾ、
_=≡≡三ミミﾐ ミﾐヾ、ソ)),,》 .
彡彡二二三≡ミ-_ ﾐﾐ|ノﾉj )||ヽ, )、
__,,,,,,,,,／彡二二二 ,- __ﾐ|/ﾉ ﾉﾉﾉﾉ) ||
-=二ミミミミ----==--'彡 ∠ミﾐ_ソノノノﾉ ﾉ
/／＞=''"二二=-'"_／ ノ''''')λ彡／
,,/￣''l 彡/-'''""￣-=彡彡／ ,,-''",,,,,,,ノ .彡''"
(, ,--( 彡 ,,-- ===彡彡彡"_,-＿ ヽ Υ
ヾ-( r'''''＼ ／／=二二''''''彡ｿ￣ ∠__＼ .＼ｿ .|
＼;;;; ＼ Ζ彡≡彡-'''',r-､> l_"t。ﾐ＼ﾉ,,r-v ／￣￣￣￣￣￣
＼;;;; ＼ 彡""彡彡-//ヽ" ''''''""￣'''""(ｴｱ/ ／
＼;; ＼'''''')彡ヽ// | (tv ／| , r_>'| ＜一体みんな誰と戦っているんだ
＼;;; ＼'" ＼ ,,"''-,,ﾉ,r-", / r'''-, .j ＼
＼;;; ＼ ／,,>--'''二"''' r-| 二'" / __ ＼＿＿＿＿＿＿
＼;;r'""彡_l:::::::::::::::::::::: /./_ " ／￣￣"===-,
)''／／rl_--::::::::::::::::/:/ヽ"'=--":
0531１３２人目の素数さん
2009/01/26(月) 09:39:21>判定するアルゴリズムも書けるし、ある特定の（例えばピタゴラスの）定理の証明で
>あるかどうかの判定をするアルゴリズムも書ける。
ええ、うそでしょ？
ならそのアルゴリズムがすでに定理の証明になっちゃってるじゃん。
0532１３２人目の素数さん
2009/01/26(月) 12:00:37を使えば、ある文字列(式)がどのような定理(型)を証明しているか、それとも間違っている(型エラー)か自動判定することができる。
しかし、逆に、定理(型)からその証明(式)を導くことは完全自動では無理。
0533１３２人目の素数さん
2009/01/26(月) 14:35:49問題を入力すると、その問題を２ちゃんやYahoo!やOKWaveとかの質問スレに自動的に書き込んで、結果を読み込んで戻ってくる。
そういう掲示板だけでなく、あらかじめ指定したアドレスへ質問メールを出して、返答を受けることも可能。
これで殆ど解決。
でも最近、回答の精度が落ちてるんだよなあ。「マルチポストはヤメレ」「質問ばかりするな」なんていう意味のない回答が良く来るようになった。
どうしてこうなったんだろう。プログラムのミスかなあ。
この辺をどう解決するかが今後の課題。
0534１３２人目の素数さん
2009/01/26(月) 17:47:35虱潰せばできるけどね
簡単な定理でも地球が滅びるくらいの時間が掛かるだろうけど
0535１３２人目の素数さん
2009/01/26(月) 19:46:43それは反則ではないのか？
0536KingGold ◆3waIkAJWrg
2009/01/27(火) 18:05:140537１３２人目の素数さん
2009/01/27(火) 23:14:04証明はDNAパソコンでしょ
0538１３２人目の素数さん
2009/01/27(火) 23:16:47そういうソフトはすでに存在しているんじゃね？
オープンにされてないだけで。
簡単につくれるし。
0539１３２人目の素数さん
2009/01/27(火) 23:26:430540１３２人目の素数さん
2009/02/06(金) 10:13:49プログラムによって解かせるものを考えた。
でもこれって既出かな？？？
0541１３２人目の素数さん
2009/02/07(土) 08:19:23ソースきぼんぬ
0542１３２人目の素数さん
2009/02/07(土) 10:07:420543１３２人目の素数さん
2009/02/07(土) 10:14:34ネタの仕込みからにぎりまで
そばロボットもいい
0544540
2009/02/07(土) 10:29:02『数学的帰納法』で
１．等式の証明
２．不等式の証明
があるけど
正の整数（自然数）のみ動かせば
負の整数の場合も自動的に掃きだしてくれる。
0545１３２人目の素数さん
2009/02/11(水) 08:53:40の証明を
P(0) かつ \forall k \in N, (P(k) => P(k+1))
を使って自動証明するってことだよね。
具体的にどんなことが自動でできるの？kwsk
0546１３２人目の素数さん
2009/02/11(水) 17:31:47論理的に式変形をしてしらみつぶしに解いていくだけ
0547１３２人目の素数さん
2009/02/11(水) 23:16:09とかも自動証明できたりする？
0548１３２人目の素数さん
2009/02/12(木) 11:49:28ぜひどうなるか知りたいね。
0549１３２人目の素数さん
2009/02/13(金) 00:10:01∀x, ∀y, x + y = y + x が自動で証明できたら
かなりすごいんじゃね？
0550１３２人目の素数さん
2009/02/13(金) 00:23:06そんな単純な問題なら一瞬で証明できるわな
0551１３２人目の素数さん
2009/02/13(金) 00:25:29してくれ
0552１３２人目の素数さん
2009/02/13(金) 00:46:340553１３２人目の素数さん
2009/02/13(金) 11:00:44してくれ
0554１３２人目の素数さん
2009/02/13(金) 16:27:06して。
0555１３２人目の素数さん
2009/02/13(金) 16:42:42頼む
0556１３２人目の素数さん
2009/02/13(金) 18:17:400557１３２人目の素数さん
2009/02/13(金) 18:54:35dim y as string
dim + as string
でできるじゃん
あとは配列にいれてソートしてイコールになればＱＥＤ
0558１３２人目の素数さん
2009/02/14(土) 00:17:140559１３２人目の素数さん
2009/02/14(土) 00:36:23わからん kwsk
0560１３２人目の素数さん
2009/02/14(土) 00:52:19定理の証明を実際的な時間で証明するのは何らかの支援が必要でしょうな。
0561１３２人目の素数さん
2009/02/14(土) 03:20:080562１３２人目の素数さん
2009/02/14(土) 03:35:032重指数時間かぁ・・・
それは絶望的だな
0563１３２人目の素数さん
2009/02/14(土) 09:19:12>>549なんかはxとyの組み合わせが無限にあるから、有限時間には終わらない。
0564１３２人目の素数さん
2009/02/14(土) 13:45:430565１３２人目の素数さん
2009/02/14(土) 16:42:350566１３２人目の素数さん
2009/02/14(土) 18:49:330567１３２人目の素数さん
2009/02/14(土) 22:46:50決定不能問題のほうがはるかに多い。
0568１３２人目の素数さん
2009/02/14(土) 23:19:480569１３２人目の素数さん
2009/02/14(土) 23:51:180570１３２人目の素数さん
2009/02/15(日) 00:28:550571１３２人目の素数さん
2009/02/15(日) 22:02:380572１３２人目の素数さん
2009/02/15(日) 22:23:290573１３２人目の素数さん
2009/02/15(日) 23:49:35EXPTIMEとかも余裕で含むので「現実的には計算不可能な」
証明がほとんどと見なして差し支えないかと。
0574１３２人目の素数さん
2009/02/16(月) 03:15:480575１３２人目の素数さん
2009/02/16(月) 18:34:58世の中から単純ソートが無くならない所以。
数値解析や数理計画のように実行回数が少ないものはO(n^3)でも歓迎されるくらいだ。
空間計算量の方はもっと厳しくて、理論上指数時間のアルゴリズムでも、
実用上はメモリの制約の方が先にやってくるというのはよくある話。
0576１３２人目の素数さん
2009/02/16(月) 19:03:20しらみつぶしにやると当然指数的に増加していくな
0577１３２人目の素数さん
2009/02/16(月) 22:51:300578１３２人目の素数さん
2009/02/16(月) 23:35:56うーん、やっぱり２とか３まで現実的か・・・
例えばＲＳＡが多項式時間で解けるようになったとして、何乗ぐらいから無意味になるの？
0579１３２人目の素数さん
2009/02/19(木) 02:35:00実数だから、0、0.1、0.001とかしらみつぶしにしても永久に１までたどり着けない。
離散数学なら4色問題とかでできるんじゃないかな。
0580１３２人目の素数さん
2009/02/19(木) 04:06:53？？？
処理のエンジン部分を開発しているチームは、日々それと格闘しているだろ。
ループの回し方１つで、処理時間のオーダーが変わる世界。
>>579
変数に代入する値をしらみつぶしとはだれも言ってないと思うが。
0581１３２人目の素数さん
2009/02/20(金) 03:27:49連続を扱えるはずがない。
お絵かきソフトで直線を書いてもドットの粒が並んでるだけだよ。
直線は絶対にかけないよ。
それどころか紙と鉛筆ですら直線は書けない。
鉛筆の分子が有限個、紙の上に並んでいるだけだから。
というかこの世は離散だから解析学は滅びるべきだよ。
実数も。
0582KingGold ◆3waIkAJWrg
2009/02/20(金) 03:30:160583１３２人目の素数さん
2009/02/20(金) 03:34:15お前がやれカス
0584KingGold ◆3waIkAJWrg
2009/02/20(金) 03:40:200585１３２人目の素数さん
2009/02/20(金) 07:35:08ムカつく奴が計算自慢してます。どうか、皆さんでそいつをギャフン(死語ｗ)と言わせてくださ！
板は・スロットサロン
スレは・しのけん
ですm(__)m
ちなみに…∫[-∞,∞]cosbxdx/(x^2+a^2)の値を求めよ、は？
みたいなのを出して答えられないとバカにしまくり。どうか、よろしくお願い致します！m(__)m
0586KingGold ◆3waIkAJWrg
2009/02/20(金) 14:15:080587１３２人目の素数さん
2009/02/20(金) 23:19:230588１３２人目の素数さん
2009/02/21(土) 00:34:010589KingGold ◆3waIkAJWrg
2009/02/21(土) 17:02:480590１３２人目の素数さん
2009/02/22(日) 00:44:020591KingGold ◆3waIkAJWrg
2009/02/22(日) 00:47:520592１３２人目の素数さん
2009/02/23(月) 10:26:02マルチ
0593１３２人目の素数さん
2009/02/28(土) 19:31:02ものの長さや、時間の流れは連続だが。
偏った"この世"じゃねーか？
実数の公理を使えば、コンピュータでも実数の性質を扱うことは出きるだろ。JK。
0594１３２人目の素数さん
2009/02/28(土) 19:50:14長さにも時間にもプランク単位、即ち最小単位があるだろ
どんな長さや時間もプランク単位の自然数倍、連続じゃないよ
0595１３２人目の素数さん
2009/03/01(日) 09:40:59｜最近では Zurek その他の研究で、量子カオス系においてはプランク定数以下のミクロ構造が現れる事が知られており、まだプランク定数の正体はよく判っていないと言えるだろう。
0596１３２人目の素数さん
2009/03/01(日) 09:52:47１プランク長 = 1.616252... × 10^(-35) [メートル]
って時点で、1メートルがプランク単位の自然数倍じゃないよ。
1メートルってのは実は存在しない長さなの？
0597１３２人目の素数さん
2009/03/01(日) 18:25:450598１３２人目の素数さん
2009/03/01(日) 19:08:040599１３２人目の素数さん
2009/03/03(火) 00:32:30ミジンコの体重がおおよそそれくらい。だからプランクトンと…
0600１３２人目の素数さん
2009/03/06(金) 13:51:430601１３２人目の素数さん
2009/03/06(金) 13:52:390602１３２人目の素数さん
2009/03/07(土) 13:11:32座布団一枚
0603１３２人目の素数さん
2009/03/09(月) 16:10:20うん、それ無理。
ペアノの公理系で、加法の交換法則は定義されてるの。
この公理をペアノの公理系の内部で定理として証明するのは
不可能だったはずよ。
0604１３２人目の素数さん
2009/03/09(月) 22:01:170605１３２人目の素数さん
2009/03/10(火) 01:18:03> >>549
> うん、それ無理。
>
> ペアノの公理系で、加法の交換法則は定義されてるの。
> この公理をペアノの公理系の内部で定理として証明するのは
> 不可能だったはずよ。
ゴルァ、シレっとウソつくんじゃねえｗｗｗｗｗ
『ペアノ数の概念について』（小野勝次・梅沢敏郎 訳・解説）、共立出版
のp.111に９という番号の付けられた
a, bεN . ⊃ . a+b=b+a
って式が定理として挙げられてるぞ。ペアノ自身の証明はそれを見ろ。
0606１３２人目の素数さん
2009/04/05(日) 16:11:55脳は分子機械に過ぎないのだから
証明は心霊現象になってしまう
0607１３２人目の素数さん
2009/04/08(水) 20:10:51http://ja.wikipedia.org/wiki/%E8%87%AA%E5%8B%95%E5%AE%9A%E7%90%86%E8%A8%BC%E6%98%8E
にでてる「ハーブランド賞」てエルブランじゃね？
0608１３２人目の素数さん
2009/04/09(木) 05:28:18Herbrandの仏語の音をカタカナで近似すれば「エルブラン」、
英語読みした音をカタカナ書きすれば「ハーブランド」
0609１３２人目の素数さん
2009/04/26(日) 22:10:30Coqのバージョン8.2ではコンパイル出来ないんですが
なぜだかわかる方居ますか？
このPDFはかなり面白そうな感じがするんですが
実際に動かせないので悲しいです
別のバージョンだと動いたりするんでしょうか
Fixpoint tupleT (A:Type) (n:nat) : Type :=
match n with
| O => unit
| S m => A * tupleT A m
end.
全般的に依存型に関する情報が少ないもので困ってます
0610１３２人目の素数さん
2009/05/03(日) 08:30:48Open Scope type_scope.
の１行を最初に書くと私の環境ではコンパイルとおりました。
Coq 8.1pl2 と8.2 でコンパイルが通ったことを確認しました。
0611１３２人目の素数さん
2009/05/03(日) 11:27:41ベジータ「数学は科学基礎だ!!
舐めるなよー!!!!｣
>>595
宇宙→銀河系→太陽系→惑星→分子→原子→素粒子→クォーク→…
無限階層説があるのう｡
0612１３２人目の素数さん
2009/05/05(火) 00:30:01動きました!
諦めかけてたのですが、ありがとうございます!
0613１３２人目の素数さん
2009/07/08(水) 17:10:040614↑
2009/08/11(火) 21:15:590615１３２人目の素数さん
2009/08/15(土) 13:26:46定理証明支援系と依存型プログラミング勉強会
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
0616１３２人目の素数さん
2009/08/15(土) 17:37:17> コンピューターによる定理の自動証明
> これが可能になったら数学者という仕事が無くなっちゃうの？
1 にマジレスすると、自動証明できる空間は非常に小さくて、ほとんど意味が無い。ということが証明されている。
むしろ多くのひとが興味のあるような命題は機械の支援に加え人間の手が必ず必要になる。
これは普通の数学だとあんまりうれしくない事実だけど、コンピュータの動作の保証が得られることは、プログラムの世界では
非常に重宝される技術。例えば、原子力施設のプログラムや、鉄道や道路の信号のシステム、医療、金融関係のシステムは不具合が許されない。
結論を言うと、定理証明の技術が発展すれば、数学者はプログラムの基幹システムにおいて、むしろ必要不可欠になる。
だから、数学者はプログラム技術を、プログラマは数学をしっかり学んでおくと将来お徳だと思う。
以上が私の妄想。
0617１３２人目の素数さん
2009/08/21(金) 22:58:470618１３２人目の素数さん
2009/08/22(土) 11:03:50実数の集合は有理数の集合より大きい濃度を持つ
0619１３２人目の素数さん
2009/09/07(月) 00:35:120620１３２人目の素数さん
2009/10/13(火) 21:35:41よくある論理パズル（正直者と嘘つきがいて、ある人が～と言った。とかいうやつ）を
coqで解きたいと思ったのですが
要するに命題論理の式をCNF(乗法標準形？）に変形できればいいのですが
coqでうまくやる方法をご存知の方いますか？
0621sage
2009/10/15(木) 16:29:240622sage
2009/10/15(木) 16:31:570623１３２人目の素数さん
2009/10/16(金) 00:37:23元の質問の動機は、スマリヤンの本の序盤のパズルを
覚えたてのcoqを電卓がわりに使って解けないかというぐらいのものなので、
ちょっと問題が大きい感じです。
hnfというtacticが標準であるので、
他の標準形にもちょいちょいと直せないものかと思った次第です。
0625１３２人目の素数さん
2009/10/16(金) 12:19:06Wikipediaにまとめがありました。
http://en.wikipedia.org/wiki/Knights_and_Knaves
日本語なら
http://www.kai.ed.jp/math/gakusyuu/2002minami.htm
というのが検索で出てきました。
よくあるパズルとか書きましたが、
スマリヤンがオリジナルなのかもしれません。
0626１３２人目の素数さん
2009/11/02(月) 13:37:580627１３２人目の素数さん
2009/11/03(火) 05:57:33どうも、「ＥＵＲＭＳ（∋ M_SHIRAISHI氏 ）の理論」のほうが正しいようだな。
例えば、《仮言三段論法の原理》は、従来は、 [(Ｐ⊃Ｑ)＆(Ｑ⊃Ｒ)]⊃(Ｐ⊃Ｒ) で
表わされるもののことと考えられていたのだっただが、これは、どうやら、誤りだった
ようだ。
そして、ＥＵＲＭＳの言う［Ｐ(ｘ)⇒/x/Ｑ(ｘ)]＆[Ｑ(ｘ)⇒/x/Ｒ(ｘ)］⇒/p,q,r/［Ｐ(ｘ)⇒/x/Ｒ(ｘ)] 1{Ｑ」
こそが、《仮言三段論法の原理》を 正しく捉(とら)えてたものと考えられる。
ＥＵＲＭＳの主張する「論理＊大＊改革」は、恐らく、世界を席巻することとなろう。
http://www.age.ne.jp/x/eurms/RONRI-J02.html#E-Books
0628１３２人目の素数さん
2010/02/04(木) 17:16:300629１３２人目の素数さん
2010/03/02(火) 21:35:271年前のレスだが、1mがプランク長の整数倍じゃないのは誤差だから。
0630１３２人目の素数さん
2010/03/02(火) 22:19:16厳密な整数倍じゃないのは単なる誤差
0631１３２人目の素数さん
2010/03/02(火) 22:43:530632１３２人目の素数さん
2010/03/06(土) 01:03:580633１３２人目の素数さん
2010/03/06(土) 02:30:58それを言うならば、そもそも選択公理を用いた数学で物理理論を記述してるのがナンセンスなのだが
フルスペックの選択公理はBanach-Tarskiのパラドックスを導いてしまうからね
>>631
うん、例えばクーロンの定義が電気素量ｅの１Ｎ（アボガドロ数）倍（つまり１モルの陽子の電荷総量）なら明解なんだけどね
現在は電流単位としての１Ａ（アンペア）をその電流が流れる電線の間の力の強さで定義して
１Ａの強さの電流で１秒流れる電気量を１Ｃ（クーロン）として定義してるからなあ
質量の単位のｋｇについても今のキログラム原器なんて怪しげというか恐ろしく原始的な定義じゃなくて
炭素１２原子核の質量の１Ｎ倍を１２グラムとして定義しようというアイデアはかなり昔からあるんだよな
あるいは陽子（普通の軽い水素の原子核）の質量の１Ｎ倍を１ｇと定義すればもっと明解だな
炭素１２原子核にしろ陽子にしろ、そういうものの質量なら質量分析器を用いて極めて精密に測れるからね
今は逆にアボガドロ数の定義として１２ｇの炭素１２に含まれる炭素１２の原子数を用いていたんじゃないかな
（つまり上の新しい定義の提案だと、アボガドロ数は実験で決まる定数でなく最初から値を定めておく定数にせねばならない）
0634１３２人目の素数さん
2010/03/06(土) 23:28:1010進数は人間の指の数が起源だからある意味原始的。日常生活での16進数への移行は難しいが
0635１３２人目の素数さん
2010/03/09(火) 13:08:15数はどの底をとっても恣意的でしょう。
もっというなら16進数よりは2進数のほうが本質だと思う。
0636１３２人目の素数さん
2010/03/10(水) 22:09:120637１３２人目の素数さん
2010/03/15(月) 12:27:50のが本質。但しこれだと０を表すことができないので、
個数に１個げたを履かせることで回避するようなことをしなければ
ならない。
たとえば
０： ×
１： ××
２： ×××
１０： ×××××××××××
。。。。
0638１３２人目の素数さん
2010/03/16(火) 01:21:49底とかナシで無限個のシンボルをつかって表現するのが本質なんじゃない？
つまりどの数も違うひとつの記号で表されるって感じで。
実際は、これを実現するのが無意味に大変だから、
「わかりやすい」とか「つかいやすい」とかの>>635のいうところの恣意的な理由で
適当な基数をきめて、その組み合わせやら式やらの一定のパターンでもって
数を表現しているわけだよね。（ここは「数学」の本質かな）
１進なら個体の数が直接的にわかりやすいから、
２進ならコンピュータであつかいやすいから、
１０進なら人間にわかりやすいから、
１６進ならコンピュータであつかいやすくて人間にもそこそこわかりやすいから、
という感じ？
こう書くと、この中では１６進が一番恣意的だな。
0639１３２人目の素数さん
2010/03/16(火) 06:48:47ハル これは。。。。。。。。自明だ。QED
0640１３２人目の素数さん
2010/04/08(木) 07:14:590641１３２人目の素数さん
2010/04/08(木) 07:50:13「それならコンピュータに解法プログラムと数式処理プログラムと人工知能を組み込んで問題を解かせることは
可能だと思われますか。もしできるなら、スーパーコンピュータのサーバーサイドに入試問題解説ソフトウェア
を組み込んで富士通のクラウドサービスで配布すれば教育費が安上がりになるはずです。」
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
0642１３２人目の素数さん
2010/04/14(水) 18:11:43あとプログラマ向けにhttp://adam.chlipala.net/cpdt/とか
0643１３２人目の素数さん
2010/04/16(金) 17:52:50どうせ本屋に取り寄せて貰っても同じだし、直接springerから買うか…
0644１３２人目の素数さん
2010/04/25(日) 20:37:340645１３２人目の素数さん
2010/04/25(日) 21:11:370646１３２人目の素数さん
2010/05/08(土) 20:35:41＞可能だと思われますか。
計算量理論などの結果からすると難しいと思うが入試問題の解法アルゴリズムについて
考察することは興味深いな。定理証明技法に基づく入試問題攻略本が書けたら売れるだろうな。
0647１３２人目の素数さん
2010/05/08(土) 22:48:380648１３２人目の素数さん
2010/05/08(土) 22:51:50ボーマン。。。アンテナがへんだわ、ちょっとみてきて
0649１３２人目の素数さん
2010/05/29(土) 13:42:260650１３２人目の素数さん
2010/06/11(金) 05:00:370651１３２人目の素数さん
2010/06/11(金) 07:20:56俺にできるチャンスがあるってことだ。
成功したら報告しに来るよ。
0652１３２人目の素数さん
2010/06/25(金) 00:50:58学んで、その結果かなりの定理が自動的に証明できるレベルに達したとする。
だが、如何なる命題を定理に据えて理論体系を構築するのかという部分は、
どうするのか？何が定理として相応しいか、何が単なる証明できる命題という
だけの単なる命題にすぎないのかをどう判定判別するのであろうか？
■ このスレッドは過去ログ倉庫に格納されています