下記(参考)引用
「 Interuniversal geometry とABC 予想61 」からだが
これは いい話だね

思うに
１）望月＆星氏は 加藤氏のLANAプロジェクトに 現状のLeanコードを公開すべきだろう
２）そして、問題点を明らかにして オープンな議論を惹起すべし
３）望月＆星氏は 今回の加藤氏のLANAプロジェクト中間発表について コメントを出すべきだろう
４）その上で、今後どうしていくのかのロードマップを公表すべきだ

要するに
衆知を集めて 遠アーベル関係者みなで議論して 解決策を模索するべし！だね
その理由は
１）IUT論文は、すでに２つ投稿され 査読掲載されている
　一つは望月氏自身のIUTの大作で もう一つは5人共著のフェルマー解決論文で Kodai mathに掲載された
　さらには、中国の若手の周忠鵬の論文もある
　さらには、日仏合同 Arithmetic & Homotopic Galois Theory IRN も進んでいる
２）このような背景から考えて、できるだけ早く 事態を収拾すべき
　混乱を長引かせるのは、よろしくない

三人寄れば文殊の知恵
問題をオープンにすべし
解決を長引かせるのはよろしくないだろう

(参考)
https://rio2016.5ch.io/test/read.cgi/math/1783860274/316-618
316１３２人目の素数さん
2026/07/20(月) ID:B6WVrHSM
>>312
もしかしてこれ？
With AI becoming increasingly capable of solving difficult problems, I've been wondering why LANA hasn't released its Lean formalization, even in an incomplete state. Even if the proofs themselves are unfinished, the definitions and overall formal framework would already be valuable to the community.

That's one of the reasons I decided to publish my own independent Lean formalization of IUT, developed with the help of Fable5. I also shared it on 4chan and 5ch in case anyone is interested in taking a look.

but, comment is japanese only.
https://github.com/Takkun-kohinata/IUT_LEAN
(google訳)
AIが難問を解く能力をますます高めている中で、LANAが未完成の状態であってもLean形式化を公開しないのはなぜだろうかと疑問に思っていました。証明自体が未完成であっても、定義と全体的な形式的枠組みは既にコミュニティにとって価値のあるものとなるはずです。
それが、私がFable5の協力を得て独自に開発したIUTのLean形式化を公開することにした理由の一つです。興味のある方がいらっしゃれば、4chanと5chにも投稿しました。

318１３２人目の素数さん
2026/07/20(月) ID:joumQYeu
>>316
それだよ
やっと承認されたか
woitの方にも似たこと書いたけど承認されんわ
(引用終り)
以上