26/06/13 09:10:06.29 TTzQJf42.net
つづき
補足
>URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)(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 だから その前という設定かな？）
つづく