26/07/20 08:40:57.28 a0+1odGL.net
>>334 補足
URLリンク(zen.ac.jp)
LANAプロジェクト
現時点での評価、残された課題、Scholze–Stix報告書との関係を報告
URLリンク(github.com)
公開文書「Project LANA Interim Report on IUT Theory」報告書全文 2026/07/17
抜粋
P44
URLリンク(i.imgur.com)
Figure 6. The η algorithm
が、キモだろう
P45
URLリンク(i.imgur.com)
直後の 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の形式化を達成してください!