>>490 追記

下世話な話だが
望月氏は、世事に疎いみたいなので書いておくと
IUTがLean形式化がパスしないと
世間からは、IUT証明はしっぱいと判定されるだろう

が、後付けでも ロジック追加で Lean形式化のギャップを埋めることができれば
一応格好はつく

さて、IUT証明しっぱいと判定されて困ることは
・まず、望月研の院生が困る
（あの有名な望月研か と言われるか 悪名高い望月研出身かとなるかのちがい）
　フェセンコ氏や彼の弟子 周忠鵬も同じ
・RIMS のIUT論文別冊出版のとき
　巻頭に編集者連名で「ちゃんと審査したので大丈夫」宣言を書いた
　柏原先生が 筆頭だったが、10名くらい居たはず
・遠アーベルプロジェクト
　”Arithmetic & Homotopic Galois Theory IRN” https://ahgt.math.cnrs.fr/activities/
　ここに 仏国の人もいるから、おおげさには国際問題

そんなこんなで 繰り返すが
後付けでも Lean形式化のギャップを埋めることができれば 一応格好はつく
が もしダメでも それは仕方ない。人間だもの
（スポーツなら 後のVAR判定で再逆転もありかも）
ともかく、事態の収束を加速する必要がある