26/06/13 09:08:29.27 TTzQJf42.net
つづき
URLﾘﾝｸ(zen.ac.jp)
プレスリリース ZEN大学 2026/03/31
IUT（宇宙際タイヒミューラー）理論のコンピューターによる検証を目指すZEN数学センターの新プロジェクト「LANA」を発表
―世界3大学による国際共同研究として始動―
x.com/ math_jin/
4/9のAIと形式化の研究集会における望月新一氏の講演動画
#IUTABC
Shinichi Mochizuki: On the Formalization of IUT: a preliminary progress report
youtube.com
Shinichi Mochizuki: On the Formalization of IUT: a preliminary...
In this talk, we survey preliminary work conducted by my research group at RIMS, Kyoto University, since the fall of 2025 on the long-term project of formali...
午前5:36 · 2026年4月16日
Shinichi Mochizuki: On the Formalization of IUT: a preliminary progress report
exlean 2026/04/15
最後に、ケーススタディとして、IUTに関する3番目の論文の最終部分「3.11⇒3.12」のロジックを、リーン形式化の観点から適切なブラックボックスに再編成した事例を詳しく解説します。これは、IUTのこの部分が最も注目を集めたためです。この部分のために作成したリーンコードの骨組みは、リーンをコミュニケーションツールとして活用した非常に成功した事例となりました。
URLﾘﾝｸ(youtu.be)
(参考)
URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
望月新一
2026年04月08日
・（過去と現在の研究）研究集会「Workshop on AI and Theorem Provers in
Mathematics」での講演のスライドを公開。
URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)(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 が 長いぜよ おい （＾＾
(参考)
URLﾘﾝｸ(www.kurims.kyoto-u.ac.jp)
[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.へ)
つづく