>>657 補足
>https://www.kurims.kyoto-u.ac.jp/~motizuki/Formalization%20of%20IUT%20(2026-04).pdf
>ON THE FORMALIZATION OF IUT: A PRELIMINARY PROGRESS REPORT [JOINT WORK IN PROGRESS WITH Y. HOSHI, G. YAMASHITA, Y. YANG, ] Shinichi Mochizuki (RIMS, Kyoto University) April 2026

これ結構おもしろい
1）”§2.First steps toward the LeanForm of IUT” Stage 1〜5
　いま Stage 1の1/3くらいか
　だが、最大の山場かもね （＾＾
　7月17日中間報告記者発表を予定
2）”§3.Brief review of inter-universal Teichmuller theory (IUT)”
　”Lean formalization”のために、Lean チームに理解してもらう必要があるんだｗ
　いままで、プロ数論屋相手だったから「論文読め」「全部書いてある」で ふんぞり返っていた
　だが、それでは ”Lean formalization”が進まない。微笑ましいね （＾＾
　で、これ まさに >>28のTerence Tao ＜“big picture”＞
　もっと早くこれをやれば良かった。が、いまからでもやる方がいい（というか やらざるを得ない）
3）”§4.Skeletal Lean code for 3.11.5 => 3.12”
　望月さん、いままでは 「3.11 => 3.12 は自明」とうそぶいていた（越川先生に対して）
　違ってたんだｗ まあ 「3.11.5 => 3.12」と反省したんだｗ
　じゃあ、本来は あるべき「3.11.5 => 3.12」が抜けていたんだよね 望月さん

さてさて、7月17日金がいまから楽しみだ （＾＾
（ICM2026 20–21 July だから その前という設定かな？）