『具体的には異なる手順から得られる2つの「実数の物差し」が本当に同じものを測っていると示せるかどうかが焦点となった。……実際にはその数値を定義する枠組み同士が一致していることを示す必要がある。』
予想以上にAIの進化が早すぎて望月さん逃げ切れない🤔
やっぱり難しそうだよな。Leanでてこずっているうちに、LLMが証明しちゃう方が早いかもしれん。
結局scholzeに指摘されたところが形式化できないと
日本語 https://www.youtube.com/watch?v=g0QLL8iYECY 英語 https://www.youtube.com/watch?v=KADN5NHmIfw
チャッピーが先に解きそう
コンピュータで形式化やると決まってからの展開が早い
数学難問ABC予想、望月新一教授の証明の問題点「絞り込めた」 ZEN大学 - 日本経済新聞
『具体的には異なる手順から得られる2つの「実数の物差し」が本当に同じものを測っていると示せるかどうかが焦点となった。……実際にはその数値を定義する枠組み同士が一致していることを示す必要がある。』
予想以上にAIの進化が早すぎて望月さん逃げ切れない🤔
やっぱり難しそうだよな。Leanでてこずっているうちに、LLMが証明しちゃう方が早いかもしれん。
結局scholzeに指摘されたところが形式化できないと
日本語 https://www.youtube.com/watch?v=g0QLL8iYECY 英語 https://www.youtube.com/watch?v=KADN5NHmIfw
チャッピーが先に解きそう
コンピュータで形式化やると決まってからの展開が早い