アカウント名:
パスワード:
在野の証明って何かしら間違っていたり正しくても相手されないよね。使いやすくて確実な定理検証システムが普及してれば学者無しでも確実な証明が保証されるのに。数学界は論文を査読とか馬鹿な事やってないで、プリンキピア・マテマティカみたいな記号論理学的な形式的な証明にコンパイルしたものをアクセプトする形にするべき。そうなってないのは現代の技術では難しいからなのかな？
自動定理証明は色々と研究ありますが、一般的には難しいようですね。特に、記法すら確立していないような新しい手法なんかは全く歯が立たないかと思います。（この証明は違うけど）
まあ、確実な定理検証システムができてしまうと、数学の証明手法が大きく変わりそうですね。量子コンピューターで（網羅的に）全ての定理を並列に検証して正しい定理を探り当てる、データマイニング的な手法が数学者の仕事になるかも。
なんとも期待したい。懸賞金市場もできればリアルマネーのマイニングにもなる。不確実かつ安すぎて挑戦する人はそこまで多くはないだろうけど。
大変なのは理解するけど、他の事を後回しにしてでも数学界が最優先に取り組むべき課題だと思う。ある程度機械可読な証明文と数学者の試行錯誤のログが溜まれば、あとはAIが学習してかなり効率的に数学者の代わりができるようになるかもしれない。
AIとか、機械にやらせるときの課題は計算結果の評価方法をどうするかですね。
最近ですとビッグデータでゴリ押しするケースも多いですが、証明なんかですと多数のゴミの山の中から欲しい結果を探し出すという苦行が結局残りそうな気がします。＃ネットで欲しい文献を探すイメージ……
より多くのコメントがこの議論にあるかもしれませんが、JavaScriptが有効ではない環境を使用している場合、クラシックなコメントシステム(D1)に設定を変更する必要があります。
※ただしPHPを除く -- あるAdmin
こういうの (スコア:0)
在野の証明って何かしら間違っていたり正しくても相手されないよね。
使いやすくて確実な定理検証システムが普及してれば学者無しでも確実な証明が保証されるのに。
数学界は論文を査読とか馬鹿な事やってないで、プリンキピア・マテマティカみたいな記号論理学的な形式的な証明にコンパイルしたものをアクセプトする形にするべき。
そうなってないのは現代の技術では難しいからなのかな？
Re: (スコア:1)
自動定理証明は色々と研究ありますが、一般的には難しいようですね。
特に、記法すら確立していないような新しい手法なんかは全く歯が立たないかと思います。（この証明は違うけど）
まあ、確実な定理検証システムができてしまうと、数学の証明手法が大きく変わりそうですね。
量子コンピューターで（網羅的に）全ての定理を並列に検証して正しい定理を探り当てる、データマイニング的な手法が数学者の仕事になるかも。
Re: (スコア:0)
なんとも期待したい。
懸賞金市場もできればリアルマネーのマイニングにもなる。
不確実かつ安すぎて挑戦する人はそこまで多くはないだろうけど。
大変なのは理解するけど、他の事を後回しにしてでも数学界が最優先に取り組むべき課題だと思う。
ある程度機械可読な証明文と数学者の試行錯誤のログが溜まれば、あとはAIが学習してかなり効率的に数学者の代わりができるようになるかもしれない。
Re:こういうの (スコア:1)
AIとか、機械にやらせるときの課題は計算結果の評価方法をどうするかですね。
最近ですとビッグデータでゴリ押しするケースも多いですが、証明なんかですと
多数のゴミの山の中から欲しい結果を探し出すという苦行が結局残りそうな
気がします。
＃ネットで欲しい文献を探すイメージ……