>>334 補足
https://zen.ac.jp/news/zmcpostevent0717
LANAプロジェクト
現時点での評価、残された課題、Scholze–Stix報告書との関係を報告
https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf
公開文書「Project LANA Interim Report on IUT Theory」報告書全文 2026/07/17

抜粋
P44
https://i.imgur.com/oX6BZ1A.jpeg
Figure 6. The η algorithm
が、キモだろう

P45
https://i.imgur.com/wXTwfgA.jpeg
直後の 9.1. The η algorithm. で
Step 1〜9まで
9.2. The main goal
9.3. Minimal structure of the η-algorithm.
がまとめか

要するに
Figure 6. The η algorithm の破線部分が
Leanの形式化で 未達成 と読みました

望月さん、星さん、山下さん・・ 他
IUTで頑張ってきた数学者の皆さん
頑張って下さい
そして、是非 Leanの形式化を達成してください！