ホイヨ
”バザード氏・・、証明は真なら「数学界は望月氏に謝罪」”

(参考)
https://news.yahoo.co.jp/articles/55ab428a6b745668d697cd8553272d9edcf22155
news.yahoo
ABC予想証明の正否、コンピューターで決着か　望月氏が打開策示す
1/2(金) 朝日新聞 （石倉徹也）

Lean研究の第一人者である英インペリアル・カレッジ・ロンドンのケビン・バザード教授（数論）は「IUT理論が正しいなら形式化を妨げる障害はない。非常に大きな成果につながる可能性はあり、挑戦の価値はある」と取材に答えた。

■証明は真なら「数学界は望月氏に謝罪」

　ただ、道のりは険しい。証明をコードに直す形式化は、複雑な式をコードに翻訳する骨の折れる作業で、ケプラー予想の場合は数十人で約10年かかった。今回のIUT理論は、700ページ以上あり、「どこがわからないのかさえわからない」と言われた難しさだ。

　結末はどうなるのか。バザード氏は、ABC予想の証明は「誤り」と判定される可能性や、作業量が膨大で検証が頓挫する可能性を上げている。もう一つの可能性は、証明が「正しい」と検証されること。「そうなれば大きな驚きとなり、数学界は望月氏に謝罪することになるでしょう」

　望月氏にもメールで問い合わせたが、返事はなかった。

（同じ記事か）
https://www.asahi.com/articles/ASTCY1BZVTCYDIFI00XM.html
朝日新聞記事
ABC予想証明の正否、コンピューターで決着か　望月氏が打開策示す
有料記事
石倉徹也2025年12月6日