「難問「ＡＢＣ予想」解明か」記事へのコメント

oldnews

[deleted user (19654)]

本家記事 [slashdot.org] (9/10) では、証明はもちろんのこと、予想自体も意味がわからんという話になっていました。
http://abcathome.com/conjecture.php [abcathome.com] が理解に役立つらしいです。
さらに専門の人が証明について考えるときは

Re:

[kurema (42872)]

Wikipediaの記事を読む限り予想自体はかなり易しいのでは？
数学者の証明なんてのは人間の読むものじゃないです。
汎用的な自動証明検証が普及して、我々一般人が証明の正しさとか流れを簡単に判断できるようになればいいですのにね。

P=NPが証明されて数学者全員首が最も望ましいシナリオですけど。

Re:

[Anonymous Coward]

P=NPだとなぜ数学者が必要なくなるのかわかりません。

Re:

[kurema (42872)]

こちら [science.srad.jp]で述べましたが、自動定理証明 [wikimedia.org]は正しい予想の場合NP完全問題 [wikimedia.org]だからです。
NP完全問題はNP問題に含まれるのでP=NPが証明された場合、そのアルゴリズムからP問題として解けます。
P問

Re:

[Anonymous Coward]

> こちらで述べましたが、自動定理証明 [wikimedia.org]は正しい予想の場合NP完全問題 [wikimedia.org]だからです。
リンク先には命題論理の自動定理証明はNP完全問題としか書かれてねーじゃん。一階述語論理という言葉の意味すら理解できなかったの? あまりにもひどすぎる。お前はもう定理の自動証明について一切語るな。

Re:oldnews

[kurema (42872)]

NP問題であるという事を示すのに天才数学者は別にいりません。
定義から、どのような問題でも多項式時間で自動証明検証ができる場合は(NP完全かはともかく)NP問題に当てはまります。
証明が有限長を持ち、各ステップの妥当性がアルゴリズムで検証できる場合はそうです。
少なくとも一般人が「数学」や「証明」といった場合、有効な書かれた証明を持ち、その正しさは客観的かつ一意に判定できる分野を指すでしょう。
そこに一階述語論理と書いてあるのはまさに、ゲーデルの不完全性定理から健全性かつ完全性を持つ二階述語論理にそのような条件が当てはまらないからです。
そういう分野では証明とは何ぞやすら難しい問題になりうるのです。それはどちらかといえば論理学の領域ではないですか。

数学の世界がどうなっているか余り詳しいわけではないので、普通に数学的証明と云える範囲で、多項式時間で機械的検証ができないような例があればご教授いただきたいところです。