「P≠NPの証明（P≠PHの証明）」記事へのコメント

こういうの

[Anonymous Coward]

在野の証明って何かしら間違っていたり正しくても相手されないよね。
使いやすくて確実な定理検証システムが普及してれば学者無しでも確実な証明が保証されるのに。
数学界は論文を査読とか馬鹿な事やってないで、プリンキピア・マテマティカみたいな記号論理学的な形式的な証明にコンパイルしたものをアクセプトする形にするべき。
そうなってないのは現代の技術では難しいからなのかな？

Re:こういうの

[fiercewinds (22740)]

自動定理証明は色々と研究ありますが、一般的には難しいようですね。
特に、記法すら確立していないような新しい手法なんかは全く歯が立たないかと思います。（この証明は違うけど）

まあ、確実な定理検証システムができてしまうと、数学の証明手法が大きく変わりそうですね。
量子コンピューターで（網羅的に）全ての定理を並列に検証して正しい定理を探り当てる、データマイニング的な手法が数学者の仕事になるかも。

Re:こういうの

[annoymouse coward (11178)]

自動定理証明のシステムが存在するなら
P＝NPになりませんか？

Re:こういうの

[fiercewinds (22740)]

NP問題も（膨大な時間を使うことができれば）コンピューターで計算することは
可能ですので、自動定理証明のシステムが存在してもP＝NPにはならないですね。

また、量子コンピューターは（NP問題を効率的に計算できる）非決定性チューリング
マシンを比較的効率的にエミュレートすることができますので、NP問題が効率的に
計算できるようになったからといってP=NPになるわけではないです。
＃量子コンピューターでも、NP完全問題は効率的に計算できないみたいですけど

Re:こういうの

[annoymouse coward (11178)]

（膨大な時間を使うことができれば）ということですね
わかりました

Re:

[Anonymous Coward]

なんとも期待したい。
懸賞金市場もできればリアルマネーのマイニングにもなる。
不確実かつ安すぎて挑戦する人はそこまで多くはないだろうけど。

大変なのは理解するけど、他の事を後回しにしてでも数学界が最優先に取り組むべき課題だと思う。
ある程度機械可読な証明文と数学者の試行錯誤のログが溜まれば、あとはAIが学習してかなり効率的に数学者の代わりができるようになるかもしれない。

Re:こういうの

[fiercewinds (22740)]

AIとか、機械にやらせるときの課題は計算結果の評価方法をどうするかですね。

最近ですとビッグデータでゴリ押しするケースも多いですが、証明なんかですと
多数のゴミの山の中から欲しい結果を探し出すという苦行が結局残りそうな
気がします。
＃ネットで欲しい文献を探すイメージ……