数学@ふたば[ホーム]


[掲示板に戻る]
レス送信モード
おなまえ
E-mail
題  名
コメント
添付File []
削除キー(記事の削除用。英数字で8文字以内)


画像ファイル名:1513389143024.jpg-(48065 B)サムネ表示
48065 BABC予想証明 Name 名無し 17/12/16(土)10:52:23 No.108066 del 5月10日頃消えます
http://www.kurims.kyoto-u.ac.jp/~motizuki/
http://m.huffingtonpost.jp/2017/12/15/mathematics-abc-prove_a_23309097/
ABC予想証明おめでとうございます
削除された記事が3件あります.見る
無題 Name 名無し 17/12/16(土)13:56:53 No.108067 del
五年か〜結構早かったね。
無題 Name 名無し 17/12/16(土)14:30:24 No.108069 del
春頃に『証明でけた』ってネットで流れたろ?
関係者がリークしてたのか!

他の研究者に渡らなくて良かったな
無題 Name 名無し 17/12/16(土)14:33:36 No.108070 del
書き込みをした人によって削除されました
無題 Name 名無し 17/12/16(土)14:34:07 No.108071 del
いや、五年前から自身のHPで公開されていて、今までは査読されてたんだから、盗まれるわけ無いでしょ。
無題 Name 名無し 17/12/16(土)14:44:48 No.108072 del
今のところ、宇宙際タイヒミュラー理論のサーベイは数えるほどしか無いけど、これで少し増えるのかな。

あと、五年前も黒田氏などが一般向けの解説本を出してたけど、来年はまた何冊か出版されそう。
無題 Name 名無し 17/12/16(土)16:26:00 No.108075 del
いやケンペ鎖の例もあるから人間任せの査読は安心できん
無題 Name 名無し 17/12/16(土)17:25:57 No.108076 del
論文を確認するだけで専門家が5年かかるという…
査読なんて一般人にはむりかと。
無題 Name 名無し 17/12/16(土)17:42:21 No.108077 del
>査読なんて一般人にはむりかと。
宇宙際幾何学の専門家は現状この人ぐらいだから大丈夫だよ〜
無題 Name 名無し 17/12/16(土)20:35:27 No.108079 del
証明の論理検証を機械でやるのは
いまいち流行っていないようだけど
何が障害なの?
無題 Name 名無し 17/12/16(土)21:04:29 No.108080 del
>何が障害なの?
計算量
無題 Name 名無し 17/12/17(日)04:43:36 No.108082 del
東大の渡邉ラボの論文不正などなどがあったから、これにはマスコミも少しの間飛びつくかな。
数学は、画像の加工とかの不正のしようがないし。

間違いがあるとすれば、「壮大なミス」って感じ。
無題 Name 名無し 17/12/17(日)05:05:44 No.108083 del
>何が障害なの?
証明支援系の数学の証明への応用は、人間の証明を「紙の証明」と呼ぶことにすると、支援系による証明の形式化は、紙の証明より基本的に長くなる。そんなに長くならない分野もあるようだけれど。
(非公式だけど、慣例で人間の証明を紙の証明と呼ぶことが多い。実際には紙上の記述ではなくても…)

そして、その計算量の見積もりは既に知られている古典的な結果でも予測が困難なものが多い。
そして、膨大な長さになったものは基本人間は読めない。ただし、支援系のシステムが安全だと保証されているなら、その支援系による機械査読そのもののチェックはその内容の全体が理解できなくても良い。

もう一つの壁は紙の証明の形式化。ここはまだ完全に自動化はできない。人力で形式化をするわけだけど、その為にはその紙の証明の分野の理解とともに、証明支援系のシステムの分野の理解が必要で、両者が協力しないと前に進まない。
無題 Name 名無し 17/12/17(日)06:53:07 No.108084 del
書き込みをした人によって削除されました
無題 Name 名無し 17/12/17(日)06:54:48 No.108085 del
>No.108083
>その計算量の見積もりは既に知られている古典的な結果でも予測が困難なものが多い。
ワカラン
定理(または証明前の予想)を与えて証明を機械に探させる(自動定理証明)ならともかく、
すでに書かれている紙の証明が演繹ルールに則っているかチェックするだけなら
以下の2点がクリアされれば計算量は問題にならないように思える

>膨大な長さになったものは基本人間は読めない。
機械査読のシステムそのものに安全性証明が必要なのはワカル
こっちはガチで自動定理証明の領分なので計算量は問題になるかもしれん
が、人間の査読を主、機械査読を参考とするなら
実用上はナアナアでもある程度役に立つかもしれん(人間の査読に対するサジェストを与えるの意味で

>もう一つの壁は紙の証明の形式化。
ワカル
無題 Name 名無し 17/12/17(日)07:26:51 No.108086 del
>すでに書かれている紙の証明が演繹ルールに則っているかチェックするだけなら
>以下の2点がクリアされれば計算量は問題にならないように思える

たしかにちょっと表現がいい加減だった。
紙の証明を証明支援系の形式表現に換えて、証明が完成したその支援系の証明の長さが、紙の証明からは今のところ予測しづらいってことね。
すごく長くなるかもしれないし、そんなに長くならないかもしれないって意味。
今後はそれ程問題じゃなくなるのかもね。
無題 Name 名無し 17/12/23(土)23:13:40 No.108127 del
書き込みをした人によって削除されました

【記事削除】[画像だけ消す]
削除キー
- GazouBBS + futaba-