… |
五年か〜結構早かったね。 |
… |
春頃に『証明でけた』ってネットで流れたろ? 関係者がリークしてたのか! 他の研究者に渡らなくて良かったな |
… |
書き込みをした人によって削除されました |
… |
いや、五年前から自身のHPで公開されていて、今までは査読されてたんだから、盗まれるわけ無いでしょ。 |
… |
今のところ、宇宙際タイヒミュラー理論のサーベイは数えるほどしか無いけど、これで少し増えるのかな。 あと、五年前も黒田氏などが一般向けの解説本を出してたけど、来年はまた何冊か出版されそう。 |
… |
いやケンペ鎖の例もあるから人間任せの査読は安心できん |
… |
論文を確認するだけで専門家が5年かかるという… 査読なんて一般人にはむりかと。 |
… |
>査読なんて一般人にはむりかと。 宇宙際幾何学の専門家は現状この人ぐらいだから大丈夫だよ〜 |
… |
証明の論理検証を機械でやるのは いまいち流行っていないようだけど 何が障害なの? |
… |
>何が障害なの? 計算量 |
… |
東大の渡邉ラボの論文不正などなどがあったから、これにはマスコミも少しの間飛びつくかな。 数学は、画像の加工とかの不正のしようがないし。 間違いがあるとすれば、「壮大なミス」って感じ。 |
… |
>何が障害なの? 証明支援系の数学の証明への応用は、人間の証明を「紙の証明」と呼ぶことにすると、支援系による証明の形式化は、紙の証明より基本的に長くなる。そんなに長くならない分野もあるようだけれど。 (非公式だけど、慣例で人間の証明を紙の証明と呼ぶことが多い。実際には紙上の記述ではなくても…) そして、その計算量の見積もりは既に知られている古典的な結果でも予測が困難なものが多い。 そして、膨大な長さになったものは基本人間は読めない。ただし、支援系のシステムが安全だと保証されているなら、その支援系による機械査読そのもののチェックはその内容の全体が理解できなくても良い。 もう一つの壁は紙の証明の形式化。ここはまだ完全に自動化はできない。人力で形式化をするわけだけど、その為にはその紙の証明の分野の理解とともに、証明支援系のシステムの分野の理解が必要で、両者が協力しないと前に進まない。 |
… |
書き込みをした人によって削除されました |
… |
>No.108083 >その計算量の見積もりは既に知られている古典的な結果でも予測が困難なものが多い。 ワカラン 定理(または証明前の予想)を与えて証明を機械に探させる(自動定理証明)ならともかく、 すでに書かれている紙の証明が演繹ルールに則っているかチェックするだけなら 以下の2点がクリアされれば計算量は問題にならないように思える >膨大な長さになったものは基本人間は読めない。 機械査読のシステムそのものに安全性証明が必要なのはワカル こっちはガチで自動定理証明の領分なので計算量は問題になるかもしれん が、人間の査読を主、機械査読を参考とするなら 実用上はナアナアでもある程度役に立つかもしれん(人間の査読に対するサジェストを与えるの意味で >もう一つの壁は紙の証明の形式化。 ワカル |
… |
>すでに書かれている紙の証明が演繹ルールに則っているかチェックするだけなら >以下の2点がクリアされれば計算量は問題にならないように思える たしかにちょっと表現がいい加減だった。 紙の証明を証明支援系の形式表現に換えて、証明が完成したその支援系の証明の長さが、紙の証明からは今のところ予測しづらいってことね。 すごく長くなるかもしれないし、そんなに長くならないかもしれないって意味。 今後はそれ程問題じゃなくなるのかもね。 |
… |
書き込みをした人によって削除されました |