つづき
https://youtu.be/H4n1XIa2flI?t=1

(参考)
https://www.kurims.kyoto-u.ac.jp/~motizuki/news-japanese.html
望月新一
2026年04月08日
　・（過去と現在の研究）研究集会「Workshop on AI and Theorem Provers in
　　Mathematics」での講演のスライドを公開。
https://www.kurims.kyoto-u.ac.jp/~motizuki/Formalization%20of%20IUT%20(2026-04).pdf
§ Skeletal Lean code for 3.11.5 => 3.12

>3.11から3.11+Remark3.9.5までの間が鬼門

鬼門ってほどでないかもよ
当たり前だが、3.11と3.11+Remark3.9.5の差分は、Remark3.9.5になる
Remark3.9.5を、なんらかの形で形式的に導けばいいだけのこと
・・・ Remark3.9.5 が 長いぜよ おい　（＾＾

(参考)
https://www.kurims.kyoto-u.ac.jp/~motizuki/Inter-universal%20Teichmuller%20Theory%20III.pdf
[3] Inter-universal Teichmuller Theory III: Canonical Splittings of the Log-theta-lattice. PDF NEW !! (2020-05-18)
P126
Remark 3.9.5. In situations that involve consideration of various sorts of regions [cf. the discussion of Remarks 3.1.1, (iii), (iv); 3.9.4] to which the log-volume may be applied, it is often of use to consider the notion of the holomorphic hull of a region.
・・・
延々と
P145
(この後 Remark 3.9.6.へ)