>>669追加
　>>611 より再録
数学予想が しばしば山登りに例えられる
abc予想山 https://en.wikipedia.org/wiki/Abc_conjecture
山の頂は見えるが、途中は雲の中だ
望月論文 IUT I〜IV https://www.kurims.kyoto-u.ac.jp/~motizuki/papers-japanese.html
これを、山のステージ I〜IVと見る
各ステージ 1000ｍ級で
4000ｍ越えが IUT IV の ”Corollary 2.3. (Diophantine Inequalities)”P54
で、abc予想の山頂直結部分
Corollary 2.2. (Construction of Suitable Initial Θ-Data) P41
が、山頂直前
いま、問題にされているのは
ステージ IIIの
Theorem 3.11. (Multiradial Algorithms via LGP-Monoids/Frobenioids)P153
　↓
Corollary 3.12. (Log-volume Estimates for Θ-Pilot Objects) P173
ここの登山道で、Lean言語でもって道筋を示すマップを作ろうとすると
「なんか 繋がってないのでは？」となった
まとめると
１）IUT以前は、abc予想山の登り方が、さっぱり分からなかったのだが
２）それにチャレンジした望月さんが、登山マップを自然言語で示した
３）それを Lean語で詳細に書こうとすると、自然言語→Lean語に出来ない部分が
　3.11.→3.12.に見つかった（いまここ）
(引用終り)

１）4000ｍ越えのabc予想山に対して
２）望月IUTで、3000mのTheorem 3.11まで来た
３）その上に 望月IUTのベースキャンプ Corollary 3.12.が見える
　しかしLean言語でLANAプロジェクトが調べると ガケ崩れで 道が繋がっていない
　普通の数学者は登れないという
４）さてどうするか？
　一案は、Theorem 3.11→ Corollary 3.12.の Lean言語で繋がる道を作ること
　（ケドラヤ案は (9-1) >>669の証明を追加できれば OKだと）
　これが難しければ、Corollary 3.12.を移動し 変形するのもありだろう

はてさて、 望月グループは どうすべきか？
（個人的アドバイスは 望月研内で 若手Lean使いを育てること。また AIのClaude とかも(なんでも良いが) AI使いを育てることだな。若手の今後のギャリア形成にもなるし）
（金か？ 川上氏が金持ち。ZEN大との共同研究にする手もある）