「ドワンゴ創業者、宇宙際タイヒミュラー理論の誤りに100万ドルの賞金を提示」記事へのコメント

はよ完璧な定理自動証明が実現して欲しい

[Anonymous Coward]

人生を数学に費やしている数学者ですら、専門以外の数学はわからんで、結果ある証明を理解している人は世界でもわずか数名、なんてことになったりする。
証明の誤りが珍しいことではないと思えば、数名の検証だって信頼できないわけで、もはや「証明」の域に達しているのか

定理証明器の原理と実装さえ何とか理解すれば、あらゆる定理証明が正しいことを、誰でも自信を持って宣言できる時代になったらいいな

Re:

[Anonymous Coward]

数学者は失業を喜ぶのかはたまた他業種の皆さんのようにネオ・ラッダイトに走るのか

Re:

[Anonymous Coward]

定理証明機は論理が正しいことを保証してくれるだけで、何を証明しているかまでは保証しないのよ。
2ちゃんねるの数学スレッドで、議論の前提となる定義が正しく構成されているかどうかで荒れているのを見たことがある。

Re:

[Anonymous Coward]

機械的に証明を検証する方法は無いというのが不完全性定理じゃなかったっけ

Re:

[Anonymous Coward]

証明の検証器をペアノ算術の範囲で一生懸命書いてるのがゲーデルの不完全性定理の証明ですね

Re:

[Anonymous Coward]

検証は機械的にできるよ。と言うか、色々と話がややこしくなってきたので、「公理から証明したい定理まで、ごくごくシンプルなルールでちょっとずつ書き換わった同値な命題をずらっと並べたもの」を証明と呼ぶような話になった。ので、命題の羅列の途中に機械的に同値だと判定出来ないようなのが混ざっていると、論理の飛躍になってしまって証明としては不完全。

じゃあ、大分前のフェルマーの最終定理の話でもなんでも、証明が完成したというなら機械的にチェックすれば良いだろ、と言うのは自分も疑問に思ってなくもないけど、まあ、そこまで分解して書き下す作業自体が大変過ぎるんじゃないかな。分解するととんでもなく長く複雑な命題になってしまう話を抽象化して纏めて証明してあっても何十ページにわたってしまうような証明なので。物議を醸した四色定理なんかは、自動証明を走らせられるところまで徹底的に書き下した上で誤り無しと判定されてたりしたはず。

不完全性定理というより、チューリングマシンの停止性判定の方が近いけど、不可能だと分かっているのは、その命題の羅列を見つける機械的案方法が無いという話。

Re:

[Anonymous Coward]

不完全性定理でそういう装置を作るのは不可能って証明されているのだと思う

Re:

[Anonymous Coward]

違う。不完全性定理は公理に矛盾がないことを証明できないと言っているだけ。