26/07/26 08:58:50.61 jgtmOrU+.net
>>520
>真 そのものズバリだが
>さっさと玉音放送を流しなさい
証明は、成立か 不成立か ２値の世界だが
数学は、勝った 負けた の世界ではない
>>後付けで証明したら
>>望月新一ではなくLean形式化チームのみの大成果
>もし、そうなっても仕方ないだろう
例え話で 補足しておくと
・望月さん 詰め将棋の長手数問題を作った。名前が ”遠アーベル流IUT”
・それを、ある将棋ソフトの解析にかけたら、ある部分で詰まないよ と出た
・それを受けて、詰め将棋作者の望月氏がどうするか？
普通は、下記
１）将棋ソフトの解析をオープンにする
２）なぜ詰まないのか？ どこか改善できないか？
３）まれに、将棋ソフトのバグの可能性もあるかもです（Lean ライブラリー不備）
で、仏国との遠アーベルの国際研究プロジェクトが 走っている
URLﾘﾝｸ(ahgt.math.cnrs.fr)
早く解決した方がいいよね
（否定か肯定か 最終結果に関わらず）
仏国にも 「どうなってんの？」「こうなっています」と オープンに全てを報告した方がいい