『具体的には異なる手順から得られる2つの「実数の物差し」が本当に同じものを測っていると示せるかどうかが焦点となった。……実際にはその数値を定義する枠組み同士が一致していることを示す必要がある。』
予想以上にAIの進化が早すぎて望月さん逃げ切れない🤔
やっぱり難しそうだよな。Leanでてこずっているうちに、LLMが証明しちゃう方が早いかもしれん。
結局scholzeに指摘されたところが形式化できないと
日本語 https://www.youtube.com/watch?v=g0QLL8iYECY 英語 https://www.youtube.com/watch?v=KADN5NHmIfw
チャッピーが先に解きそう
コンピュータで形式化やると決まってからの展開が早い
はてブにでてる読売の記事見るにそれこそ禅問答みたいだった部分が人間が理解できる形になったようで、形式化の努力もいいがその時点でもう一度その道のプロが検討できるのでは？
これ学術誌に掲載されたから証明完了になったんじゃなかったっけ？もし不備があるとするなら査読した人たちの権威はどうなるのか？
ZEN大学頑張ってるのにpopopoときたら（関係ない）
証明の証明。
理解できる人が少ない、プログラムに落とし込めない、問題点がなかなか「絞り込めない」なんてモノは数学として意味あるの？いやなんも知らんからそんなものなんだよと言われたらそうなのかと思うだけだけど。
天才が合ってるかよくわからんものを出して周りが困るってフェルマー予想を連想してしまう。今回はAIのおかげで何百年もかからない。
論文の誤りを指摘されたのが2018年なので素人から見ると進んでんだか進んでないんだかわからないわね
位相空間みたいな集合の論理で進めていく抽象的な証明は、学部レベルの「正解」がある問題でも「え？なんでコレで証明したことになるの？」ってなる。最先端の理論になると、トップ数学者も自分と同じ反応になるのね
Leanで証明しようとしている
ふーん
お膝元の京大ともう1つイギリスの大学でしか扱ってないみたいな話を昔聞いてもうダメなのかと思っていたが、そうでもなかったのね
深い内容はわからないが、この話題には以前から興味があった。
数学難問ABC予想、望月新一教授の証明の問題点「絞り込めた」 ZEN大学 - 日本経済新聞
『具体的には異なる手順から得られる2つの「実数の物差し」が本当に同じものを測っていると示せるかどうかが焦点となった。……実際にはその数値を定義する枠組み同士が一致していることを示す必要がある。』
予想以上にAIの進化が早すぎて望月さん逃げ切れない🤔
やっぱり難しそうだよな。Leanでてこずっているうちに、LLMが証明しちゃう方が早いかもしれん。
結局scholzeに指摘されたところが形式化できないと
日本語 https://www.youtube.com/watch?v=g0QLL8iYECY 英語 https://www.youtube.com/watch?v=KADN5NHmIfw
チャッピーが先に解きそう
コンピュータで形式化やると決まってからの展開が早い
はてブにでてる読売の記事見るにそれこそ禅問答みたいだった部分が人間が理解できる形になったようで、形式化の努力もいいがその時点でもう一度その道のプロが検討できるのでは？
これ学術誌に掲載されたから証明完了になったんじゃなかったっけ？もし不備があるとするなら査読した人たちの権威はどうなるのか？
ZEN大学頑張ってるのにpopopoときたら（関係ない）
証明の証明。
理解できる人が少ない、プログラムに落とし込めない、問題点がなかなか「絞り込めない」なんてモノは数学として意味あるの？いやなんも知らんからそんなものなんだよと言われたらそうなのかと思うだけだけど。
天才が合ってるかよくわからんものを出して周りが困るってフェルマー予想を連想してしまう。今回はAIのおかげで何百年もかからない。
論文の誤りを指摘されたのが2018年なので素人から見ると進んでんだか進んでないんだかわからないわね
位相空間みたいな集合の論理で進めていく抽象的な証明は、学部レベルの「正解」がある問題でも「え？なんでコレで証明したことになるの？」ってなる。最先端の理論になると、トップ数学者も自分と同じ反応になるのね
Leanで証明しようとしている
ふーん
お膝元の京大ともう1つイギリスの大学でしか扱ってないみたいな話を昔聞いてもうダメなのかと思っていたが、そうでもなかったのね
深い内容はわからないが、この話題には以前から興味があった。