IUT理論のコンピューターによる検証を目指すLANAプロジェクト、 「Project LANA Interim Report on IUT Theory」を公開

現時点での評価、残された課題、Scholze–Stix報告書との関係を報告

ZEN大学の研究所「ZMC（ZEN　Mathematics　Center；ZEN数学センター）」は、2026年7月17日（金）、IUT（宇宙際タイヒミュラー）理論のコンピューターによる検証に関する「LANAプロジェクト」の中間発表会「LANA Project Interim Report July 2026」を開催しました。

本発表では、LANAプロジェクトの概要を改めて説明するとともに、現時点でのIUT理論に対する評価と残されている課題、2018年のScholze–Stix報告書との関係、今後の研究の展望、ならびに日本におけるLean形式化コミュニティ形成の取り組みについて報告しました。また、発表に合わせて、現時点での到達点をまとめた文書「Project LANA Interim Report on IUT Theory」を公開しました。

☑公開文書「Project LANA Interim Report on IUT Theory」概要

この報告書は、LANAプロジェクトがこれまで進めてきたIUT理論の検証作業について、現時点での到達点と今後の課題をまとめた中間報告です。まず、IUT理論が発表されて以降の経緯と、それをめぐる議論の流れを整理し、LANAプロジェクトがどのような立場から検証を進めてきたのかを説明します。そのうえで、少なくとも多くのプロジェクトメンバーにとって、IUT理論の第3論文の、定理3.11から系3.12を導く過程に不明瞭な点があることを指摘します。

問題点は、q-pilot対数的体積の二つの計算が「tautologicalに同値」とされている点、あるいは、アルゴリズムの出力から得られる複数の可能なデータのうちの一つが、入力から定まるデータとどのように同一視されるのか、といった点について、IUT理論の原論文の記述は明瞭に追跡可能とは言えないという点にあります。報告書は、2018年のScholze–Stix報告との関係にも触れつつ、IUT理論の正否について最終判断を急がず、論点を整理し、今後の研究、国際的議論、形式化作業の基盤を示すことを目指すと述べています。

報告書全文 ▶ https://github.com/katobungen/LANA_report_202607/blob/pdf/LANA_report_202607.pdf

☑IUT理論検証の現状と今後の見通し

LANAプロジェクトでは、2026年3月31日の公表以後も、IUT理論に関して国内外のメンバーによる集中的な討議を継続してきました。現時点におけるLANAプロジェクトの立場は、3月31日の記者会見で表明したものと同じです。すなわち、現時点におけるLANAプロジェクトは、IUT理論によってabc予想の証明が得られたか否かの判断を、引き続き保留します。数学的なギャップが存在する可能性は排除していませんが、それが本当にギャップであるのか、それともまだLANAプロジェクトメンバーの理解が十分に深まっていないことに由来するのかについては、最終的な判断を保留しています。

今後、LANAプロジェクトは、残された論点のさらなる精密化を進め、最終的にはLeanコードへ翻訳できる形に整えていきます。また、望月氏との対話を継続しつつ、LANAプロジェクトとしての独立した検証を続けていきます。それとともに、遠アーベル幾何学のLeanによるライブラリ構築や、日本におけるLean形式化コミュニティの形成にも取り組んで参ります。

 ☑関係者からのコメント

【若山正人　ZEN大学 学長】

ZEN大学はオンライン大学として新しい学びの機会を社会に開くとともに、大学として、その基盤となる学術研究を重要な柱に位置づけています。LANAプロジェクトは、従来の大学組織では取り組み難いような困難で論争的な部分もある課題に、知的な誠実さをもって真摯に向き合う、ZEN大学にとって象徴的な取り組みのひとつです。

数学の世界では、Leanによる形式化やAIとの連携によって、証明の確認と共有のあり方が大きく変わりつつあります。しかし、その基礎にあるのはあくまでも人間による深い理解と考えです。今回の中間発表が、IUT理論の検証だけでなく、日本におけるLean形式化コミュニティの形成にとっても重要な機会となることを期待しています。

【加藤文元　ZEN大学教授・ZMC所長、LANAプロジェクトリーダー】

LANAプロジェクトは、遠アーベル幾何学とIUT理論という現代数学の最前線に対して、Leanによる形式化という新しい方法で取り組む国際共同研究です。私たちは、IUT理論の正否について結論を急ぐのではなく、何が理解でき、何がなお理解できていないのかを、できるだけ率直かつ正確に言語化することを重視してきました。

現時点で我々は、IUT理論によってabc予想が証明されたかどうか、断定することはできませんでした。しかし、今後も残された論点を数学的に明確な形にし、望月氏および京都大学数理解析研究所（RIMS）側との対話も続けながら、あくまでも偏らない立場で検討を進めていきたいと思います。

❙ LANAプロジェクトについて

LANAは「Lean for ANAbelian geometry」の略称です。プロジェクトの目的は大きく二つあります。第1の目的は、日本人研究者が世界を牽引してきた数論幾何学の重要分野である遠アーベル幾何学（anabelian geometry）の主要定理を、証明支援系Leanを用いて形式化し、そのライブラリを構築することです。第2の目的は、京都大学数理解析研究所(RIMS)の望月新一教授が提唱したIUT理論を、Leanによる形式化を通じて検証することです。

本プロジェクトは、準備期間を含めると2023年秋から活動を開始し、2024年9月から本格的に始動しました。ZMCは、特定の立場に偏ることなく中立的な視点を保ちながら、IUT理論を形式化可能な形に整え、論点を明確化し、最終的には形式化することを目指しています。

❙ ZEN大学について

ZEN大学は、最先端のIT技術を活用し、すべての人に大学進学の機会を提供します。ZEN大学唯一の学部である「知能情報社会学部」では、特定の学問領域に偏らない学びを修めることで、変化し続ける社会において活躍するために必要なリテラシーを身につけることができます。さらに詳しい情報は、ZEN大学のウェブサイトおよびパンフレットをご覧ください。

ZEN大学に関する詳細▶ https://zen.ac.jp/

最新パンフレット請求▶ https://zen.ac.jp/form

開学初年度の実績▶ https://zen.ac.jp/presentation_2026/