LANAプロジェクト、IUT理論の検証に向けた中間報告を発表

LANAプロジェクトが発表したIUT理論の中間報告

2026年7月17日、ZEN大学の「ZEN数学センター（ZMC）」で、IUT理論の検証に向けた「LANAプロジェクト」の中間報告会が開催されました。このプロジェクトは、数学界の難題であるIUT理論のコンピューターによる検証を目指しており、発表された報告書「Project LANA Interim Report on IUT Theory」では、これまでの進捗や今後の課題が整理されていました。

中間発表会の概要

発表では、プロジェクトの全体像と共に、IUT理論に関する現在の評価、残された課題を共有しました。また2018年のScholze–Stix報告書との関係や、今後の研究展望、日本のLean形式化コミュニティの形成に向けた取り組みも説明されました。現時点での達成をまとめた文書も公開され、注目を集めました。

IUT理論の検証活動

報告書は、IUT理論という新たな提案に対する検証作業の進行具合を詳述。特に注目すべきは、IUT理論の第3論文における特定の定理に対する解釈の不明瞭さが示されたことです。具体的には、q-pilot対数的体積の計算に関する主張が「tautologicalに同値」とされている点や、アルゴリズムの出力から得られるデータの一貫性についての疑問が提起されました。

未来への展望

LANAプロジェクトのメンバーは、IUT理論によってabc予想が証明されたかどうかに関して、最終的な判断を保留しています。数学的なギャップの存在を否定することはできませんが、それが理解不足によるものかどうかは未解決です。今後は、残された論点のさらなる洗練を目指し、最終的にはLeanコードへの翻訳を進める予定です。

また、望月新一教授との対話を続けつつ、独自の検証を行うとのことです。さらに、遠アーベル幾何学に関連するLeanによるライブラリの構築や、Lean形式化コミュニティの発展にも取り組む方針です。

関係者のコメント

ZEN大学の若山学長は、LANAプロジェクトの重要性を強調し、オンライン教育を通じて、数学の検証や理解の方法を変えつつあることに期待を寄せました。一方、加藤教授は、結論を急がず、現在の理解と未解決の点を明確にすることの重要性を訴えました。

LANAプロジェクトの詳細

LANAプロジェクトは「Lean for ANAbelian geometry」の略であり、遠アーベル幾何学の主要定理をLeanを用いて形式化し保存することと、IUT理論の検証を狙いとしています。本プロジェクトは2023年秋から活動を始め、2024年9月以降には本格的に始動する予定です。ZEN大学の中立的な立場から、IUT理論を形式化し、その議論を明確化することを目指しています。