>>251 補足
>今からでも ギャップを埋められるか否か
>問題は、その一点じゃね？

時代が進まないと、ギャップに気付かないということは
数学史上しばしばあった

例えば、名誉教授スレで取り上げた リーマンの函数論
https://www.iwanami.co.jp/book/b458089.html
代数函数論 岩波
岩澤健吉 著 刊行日2019/07/26
＜試し読み＞
https://www.iwanami.co.jp/moreinfo/tachiyomi/0063357.pdf
緒言
Riemann は更にAbel積分を精密に考察して，後にRochによって補充されたいわゆるRiemann-Rochの定理を証明し，また一般のtheta函数を定義してJacobiのUmkehrproblemを完全に解決した．このように我々はRiemann において今日の古典的代数函数論が事実上ほとんど完成されていることを見るのである．しかしながら現在の我々の立場から見てRiemannの叙述が種々の点で厳密性を欠いていることはやむを得ない．抽象代数学も位相幾何学も未だ生れていなかった当時のことを思えばこれはむしろ当然であろう．
(引用終り)

要するに、もし Riemannの原証明を LEANにかけたら ギャップありとなるだろうが
しかし、後世 Riemannの定理には後世において 厳密な証明が与えられた

同様の例が、ガウスの学位論文 代数学の基本定理（＝代数方程式は複素数根を持つ）
の証明にギャップがあったが、後世になって修正された

そんな例は、山ほどある
LEANの結果を公開しないのは、まずは望月氏に優先的に修正のチャンスを与えようってことだろう

もし、第三者が修正案を出して それが正解なら
IUT証明の最後のレンガを積んだ人は だれだ？ となる