わたしの考えこと

数学の定理をコンピュータで証明できるか

数学の定理をコンピュータで証明することは理論的には可能であるらしい。

 

そのためには、まず、数学を形式化しなければならない。すべてを記号の操作で機械的に定理を導けるようにすることである。そして、形式化した数学をコンピュータに読み取らせるために、プログラム言語で書き換えなければならない。

 

数学は、前提となる公理を推論規則で変形することで定理を導く。よって、形式化もプログラム化も理論的には可能である。実際、数学の定理を証明するコンピュータは存在する。

 

しかし、そのコンピュータが導きだす定理は、お世辞にも意味のある定理とはいえないらしい。ほとんど、ゴミのような定理ばかりを導き出すそうである。

 

数学の定理を導く過程のパターンは、指数爆発どころではない恐ろしい計算爆発になる。しらみつぶしに計算するコンピュータでは、何億年かかっても、意味のある定理を導けないだろう。

 

この点、人間の数学者は、論理だけでなく、直感力というコンピュータにはない武器を使って、意味のある定理にたどり着くことができる。これに対して、コンピュータには直観力がないので、意味のある定理にたどり着けない。

 

結局、コンピュータが、意味のある定理を導くことはこれからもないであろう。

 

 

 

コンピュータで数学の定理は証明できる？

 

数学の定理をコンピュータで証明させようとしたら、指数爆発どころではないほどの計算爆発になる。その上、コンピュータで証明させるほど数学は形式化されていない。つまり、コンピュータで数学の定理を証明させることは夢のまた夢だ。アラン・チューリングも天国で残念がっていることだろう。 約23時間前 webから

デジタルデータ収集能力向上で未来予測もできる？

現代の統計学でも、ベイズの定理や正規分布などの２００年以上の前の数学が使われている。数学の手法自体は進歩していない。ただ、コンピュータの発明のおかげで、膨大な量のデータを収集処理できるようになった。コンピュータの「腕力」の向上で、２１世紀は正確な未来予測ができるかもしれない。 約23時間前 webから

 

チャイティンの定数

転載　

 

 

　　　　　　　　　　

 

 

http://ja.wikipedia.org/wiki/チャイティンの定数　より
「チャイティンの定数（英: Chaitin's constant）は、計算機科学の一分野であるアルゴリズム情報理論の概念で、無作為に選択されたプログラムが停止する確率を非形式的に表した実数である。グレゴリー・チャイティンの研究から生まれた。停止確率（英: Halting probability）とも。
停止確率は無数に存在するが、Ω という文字でそれらをあたかも1つであるかのように表すのが普通である。Ω はプログラムに使われている符号化方式に依存するため、特定の符号化に依存しないことを示すときは Chaitin's construction と呼ぶことがある。
個々の停止確率は正規数でかつ超越数であり、計算不可能（その数字を列挙していくアルゴリズムは停止しない）である。
・・・
停止確率の定義
接頭属性のある完備計算可能関数 F の定義域を PF とする。すると、定数 ΩF は次のように定義される。

画像：Ω

ここで、 は文字列 p の長さである。これは、F の定義域にあるそれぞれの p に対応する1つの被加数の級数である。定義域は接頭属性を持つ必要があるため、クラフトの不等式を考慮すると、この総和は0から1の間の実数に収束することが保証される。文脈上 F が明らかであれば ΩF を単に Ω と記することができるが、接頭属性のある完備計算可能関数が異なれば、Ω の値も異なる。

数論の未解決問題への応用
チャイティンの定数は原則的に、ゴールドバッハ予想やリーマン予想といった数論の未解決問題を解くのに役立つと考えられる[1]。ゴールドバッハ予想とは、2より大きい全ての偶数は2つの素数の和で表せる、というものである。ある偶数が与えられたとき、それを2つの素数の和に分解するプログラムを考える。ゴールドバッハ予想が正しければ、このプログラムは偶数を次々に2つの素数に分解していくだろう。素数に分解できない偶数という反証が見つかった場合、プログラムは停止し、ゴールドバッハ予想は間違いだったことが示される。このプログラムの長さを N ビットとする。計算資源と時間に制限がない場合、チャイティンの定数を使ってゴールドバッハ予想を次のように証明できる。同時並行的に N+1ビット以下の全てのプログラムを実行する。Nビットのゴールドバッハプログラムが停止すれば、予想は偽であったと証明される。ゴールドバッハプログラムが停止していない状態で、チャイティンの定数で示される割合を1つでも超える個数のプログラムが停止したら、ゴールドバッハプログラムは停止しないと証明され、ゴールドバッハ予想が正しいことが証明される。この手続きを行うには、チャイティンの定数の N+1 ビットまでの数値が分かればよい。

同様に、リーマン予想などの数学上の未解決問題の多くも、チャイティンの定数を使って証明（または反証）できる。」

 

転載元　http://blogs.yahoo.co.jp/crazy_tombo/37543986.html

数学の限界について

日経サイエンス2006年６月号

ゲーデルを超えて　オメガ数が示す数学の限界

G. チャイティン

http://www.nikkei-science.com/page/magazine/0606/images/0606_06.gif

 

数学の論理構造は完璧──というのは実は幻想にすぎない。かつてゲーデルの「不完全性定理」がこの事実を示したが，いま注目されるのは「オメガ」という数だ。完全に定義でき，確定値を持つのに，決して計算しきれない数とは？
　
ゲーデルは，数学が不完全であり，きちんと証明できないにもかかわらず正しい記述を含んでいることを示した。ところが「オメガ」という特別な数は，数学にさらに大きな不完全性が存在することを明らかにした。有限個の公理をいかに組み合わせても証明できない定理が，無数にあるのだ。したがって数学の「万物理論」はありえない。
　
オメガは，あるコンピューターに関して考えうるすべてのプログラムの集合から１つのプログラムをランダムに選んだ時，そのプログラムがいずれ停止するものである確率だ。完全にきちんと定義され，決まった値を持つ。しかし，どんな有限プログラムを使っても，オメガのすべての桁の値を計算し尽くすことは不可能。言い換えると，証明不能な数学的事実が無数に湧き出る泉のようなものだ。
　
この特性は，数学者が新しい公理をもっと仮定してよいことを示している。物理学者が実験結果をもとに論理的証明のできない基本法則を導くのと同様だ。
　
これら一連の結果は「アルゴリズム的情報理論」に基づいている。ライプニッツは300年以上も前にアルゴリズム的情報理論の多くの考え方を予想していた。

 

http://www.nikkei-science.com/page/magazine/images/keyword.gif

ライプニッツ／既約／充足根拠律／チューリングの停止問題／擬経験的／P≠NP問題／実験的数学

著者

Gregory Chaitin

IBMワトソン研究所の研究員で，ブエノスアイレス大学の名誉教授，オークランド大学の客員教授でもある。コルモゴルフ（Andrei N. Kolmogorov）とともに，アルゴリズム的情報理論という新領域を切り開いた。９冊の著書があり，一般的な本としては『セクシーな数学』（2002年，邦訳は2003年）や『Meta Math!』（2005年）がある。数学の基礎について考えていない時は，ハイキングや雪山歩きを楽しんでいる。

原題名

The Limits of Reason（SCIENTIFIC AMERICAN March 2006）