慌てる乞食は貰いが少ない 2026年7月17日を待て
https://zen.ac.jp/news/zmcpostevent0331
2026/03/31 プレスリリース ZEN大学
IUT(宇宙際タイヒミューラー)理論のコンピューターによる検証を目指すZEN数学センターの新プロジェクト「LANA」を発表 世界3大学による国際共同研究として始動
2026年7月17日 LANAプロジェクトに関して、活動の中間報告記者発表を予定しています。IUT理論の検証について、その時点での検証結果を詳しく公表する計画です

https://youtu.be/2jgBBw6XjQ4?t=218
ZEN数学センター IUT理論の計算機検証に関する新プロジェクト「LANA」発表 ニコニコニュース 2026/03/31
【概要】
日時：2026年3月31日 若山正人(ZEN大学長)、加藤文元(ZEN大学教授)他
コメント
@saburousaitoh
3 週間前
素晴らしい研究計画ですね。　真相が明かにされるのは　時間の問題と期待されますが、是非に及ばず、方法が　今後の数学のあり様に　甚大な貢献がなされると期待されますね。これを機会に　日本の数学界が　新しい時代に後れを取らないように期待したい

https://www.kurims.kyoto-u.ac.jp/~motizuki/news-japanese.html
望月新一
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
P2
§1. Lean formalization ( LeanForm) as a communication tool
P4
§2.First steps toward the LeanForm of IUT
The main strategy for the LeanForm of IUT:
Stage 1: [IUTchIII] Theorem 3.11 => Corollary 3.12 (since this has received the most public attention!)
Stage 2: Proof of [IUTchIII] Theorem 3.11 modulo [IUTchI-II]
Stage 3: [IUTchI-II] modulo earlier results (1995- 2015) on anabelian geometry/Frobenioids/theta functions, etc.
Stage 4: Earlier results (1995- 2015): [pGC], [GeoAn], [AbsAnb], [NCBel], [AbSc], [SemiAn], [QuCnf], [CbGC], [Con g], [FrdI-II], [EtTh], [GenEll], [NodNon], [AbsTopI-III]
Stage 5: Numerical aspects ([IUTchIV], [ExpEst])
(We are currently in the early skeletal portion of Stage 1.)
P6
§3.Brief review of inter-universal Teichmuller theory (IUT)
P9
§4.Skeletal Lean code for 3.11.5 => 3.12
P11
We chose to concentrate on this aspect of the theory rst since this aspect of the theory i.e., Stage 1: [IUTchIII] Theorem 3.11 => Corollary 3.12 (cf. the discussion at the beginning of 2) hasreceived the most public attention. Indeed, this aspect corresponds to the essential nontrivial content of the theory, i.e., that the height of the elliptic curve under consideration is equal to N times the height of the elliptic curve (where N is a large positive number), up to a small discrepancy (arising from (Ind1,2,3) + hull), thus implying a bound on the height.