26/07/25 13:42:05.74 AuqA/R3q.net
>>490 追記
下世話な話だが
望月氏は、世事に疎いみたいなので書いておくと
IUTがLean形式化がパスしないと
世間からは、IUT証明はしっぱいと判定されるだろう
が、後付けでも ロジック追加で Lean形式化のギャップを埋めることができれば
一応格好はつく
さて、IUT証明しっぱいと判定されて困ることは
・まず、望月研の院生が困る
（あの有名な望月研か と言われるか 悪名高い望月研出身かとなるかのちがい）
フェセンコ氏や彼の弟子 周忠鵬も同じ
・RIMS のIUT論文別冊出版のとき
巻頭に編集者連名で「ちゃんと審査したので大丈夫」宣言を書いた
柏原先生が 筆頭だったが、10名くらい居たはず
・遠アーベルプロジェクト
”Arithmetic & Homotopic Galois Theory IRN” URLﾘﾝｸ(ahgt.math.cnrs.fr)
ここに 仏国の人もいるから、おおげさには国際問題
そんなこんなで 繰り返すが
後付けでも Lean形式化のギャップを埋めることができれば 一応格好はつく
が もしダメでも それは仕方ない。人間だもの
（スポーツなら 後のVAR判定で再逆転もありかも）
ともかく、事態の収束を加速する必要がある