先月LEANについてこのブログで触れました。望月先生のABC予想の解決が誤っているというフィールズ賞受賞者もいるので、証明支援系と言われる関数型プログラミング言語のひとつであるLEANをつかって万人になっとくできるような定式化をするとよいなぁという話です。望月先生も今年の年頭にブログ記事でLEANの活用について期待を表明されていました。
先日、Zen大学から遠アーベル幾何学の形式化とそのライブラリ構築を第一の目的として、京都大学数理解析研究所の望月新一教授による宇宙際タイヒミュラー理論、いわゆるIUT理論を、同じくLeanの形式化によって検証することを第二の目的とする新プロジェクトLANAが発表されました。LEANの世界のトップレベルの専門家や遠アーベル幾何学の専門家が参加して、実は一年半以上前から動いていたLEANプロジェクトの公開でした。
どのようなプロジェクトかというのは、次の動画と、Zen大学から公開された主要部分の原稿を読まれるとよくわかると思います。その中で、メンバーの一人のKiran Kedlaya教授（USCD：University of California, San Diego）は、2018年のショルツェとスティックス（Scholze–Stix）の文書における「矛盾」の指摘は、意味のあるものではなく単なるコミュニケーションの齟齬に起因するものだと確認したと断言しておられます。
ZEN数学センター・新プロジェクト「LANA」の発表
https://www.youtube.com/live/b9ZV-4T3iUo
この動画中の各参加者の発言をまとめた文書が公開されているのでまず動画をみる前に読んでみてください。
『LANA プロジェクト発表にあたって』
2026.03.31 2026年3月31日に行われたLANAプロジェクト発表に際しての各員のコメントを掲載いたします。
https://zen.ac.jp/zmc/topics/jwz-o8xr3v6f