ZEN大学「ZMC（ZEN Mathematics Center:ZEN数学センター）」は、2026年3月31日（火）、新プロジェクト「LANA」を発表しました。LANAは、ZEN大学（日本）、ユトレヒト大学（オランダ）、アルバータ大学（カナダ）を中心とする国際共同研究プロジェクトであり、数論幾何学の重要分野である遠アーベル幾何学の形式化と、京都大学数理解析研究所の望月新一教授による宇宙際タイヒミュラー理論（IUT理論）の検証を主な目的としています。
 
本プロジェクトは、準備期間を含めると2023年秋から水面下で活動を続けてきました。3月31日に東京都内で開催された本件の発表会では、LANAプロジェクトの結成の経緯、目的、基本方針、コアメンバー、現時点での活動状況、そして今後の見通しについて初めて公表しました。
 
☑︎LANAプロジェクトについて
LANAは「Lean for ANAbelian geometry」の略称です。プロジェクトの第一の目的は、日本人研究者が世界を牽引してきた数論幾何学の重要分野である遠アーベル幾何学の主要定理を、証明支援系Leanを用いて形式化し、そのライブラリを構築することです。第二の目的は、IUT理論をLeanによって形式化し、その検証を行うことです。
 
Leanは関数型プログラミング言語であり、それ自体が数学の定理を自動的に証明するものではありません。通常、日本語や英語などの自然言語と数式によって記述される数学の議論をLeanの言葉で形式化するには、曖昧さをできるだけ排除しながら書き換えていく必要があります。とりわけIUT理論のような巨大で複雑な理論においては、この作業は単なる機械的な変換ではなく、理論そのものに対する深い専門的理解を前提とするものです。
 
LANAプロジェクトは、特定の立場に偏ることなく中立的な視点を保ちながら、IUT理論を形式化可能な形に整え、その検証を行うことを目指しています。理論の正否をめぐって現在も数学者たちの意見が分かれているなかで、論点をより明確にし、共有可能な形で提示することが本プロジェクトの重要な意義です。
 
☑︎結成の経緯
LANAプロジェクトの構想の背景には、近年の数学の形式化の大きな進展があります。とりわけ、フィールズ賞数学者ペーター・ショルツェ（Peter Scholze）氏の提起を契機として始まった「Liquid Tensor Experiment」は、現代数学の高度な議論がLeanを用いて実際に検証されうることを示した象徴的な事例でした。このプロジェクトを主導したヨハン・コメリン（Johan Commelin）氏とアダム・トパーズ（Adam Topaz）氏は、今回のLANAプロジェクトの中心メンバーでもあります。
 
こうした先行事例を受けて、ZMCでは、形式化という方法を通じて現代数学の重要理論に新たな形で向き合う可能性を検討してきました。その結果として始動したのが、国際共同研究としてのLANAプロジェクトです。
 
☑︎LANAプロジェクト　中心メンバー
加藤文元（ZEN大学教授・東京科学大学名誉教授、プロジェクトリーダー）
ヨハン・コメリン/Johan Commelin（ユトレヒト大学助教）
キラン・ケドラヤ/Kiran Kedlaya（カリフォルニア大学サンディエゴ校 教授）
星裕一郎（京都大学 数理解析研究所 准教授）
アダム・トパーズ/Adam Topaz（アルバータ大学 准教授）
 
このほか、学生や博士研究員（ポスドク）など若手メンバーも約7名（3ヵ国・地域）参加しており、国際的かつ多層的な研究体制のもとで活動を進めています。
 
☑︎IUT理論検証の現状と今後の見通し
LANAプロジェクトでは、1年以上にわたり、日本、カナダ、オランダ、アメリカなど各地で合宿や集中的な研究会を重ねながら、IUT理論の理解と検証に取り組んできました。その結果、現時点では研究チームとしてどこまで理解が及んでいるか、またどこが理解の及ばないポイントであるかが、かなり明確に浮かび上がってきています。さらに、我々の理解が及んでいないポイントを、できる限り平易な数学の言葉で表現するための整理も進んでいます。
 
2026年7月17日（金）には、LANAプロジェクトに関して、活動の中間報告記者発表を予定しています。IUT理論の検証について、その時点での検証結果を詳しく公表する計画です。
☑︎コメント
若山正人（ZEN大学 学長）
ZEN大学は、本格的なオンライン大学をつくることによりわが国の深刻な教育格差の緩和・解消を図るために昨年4月に開学しました。インターネットやAIなどの最新のIT技術を駆使することで、既存の大学では実現が難しかった新しい大学教育の形を作り上げることを目指しています。
一方で、大学である限り、教育を底から支え人類の知的財産を豊かにする研究もまた大きな柱です。本学では、既存の大学ではあまり取り組んでいなかったいくつかのテーマの研究を組織的に進めています。コンピューターの計算能力の飛躍的進歩に立脚した最先端の数学におけるZEN数学センターの国際プロジェクト「LANA」はその一つであり、本学の新しい挑戦と位置付けています。
加藤文元
（ZEN大学 教授／ZMC所長、LANAプロジェクトリーダー）
LANAプロジェクトは、遠アーベル幾何学とIUT理論という現代数学の最前線に対して、証明支援系Leanによる形式化という新しい方法で取り組む国際共同研究です。IUT理論は巨大で複雑であり、その正否をめぐっては現在でも世界の数学者たちの意見が分かれています。私たちは最高のスタッフを集め、1年以上にわたってこの理論について議論を重ねてきました。その結果、現時点でどこまで理解が及び、どこがなお解明できないポイントであるのかが、かなり明確になってきたと考えています。 ただし、それが本当に数学的なギャップなのか、それとも私たち自身の理解の問題なのかについては、現時点では結論を出していません。だからこそ、今後もあくまでも中立的な立場から検討を続け、望月氏との対話も進めていきたいと考えています。7月17日の中間報告では、その時点までの私たちの理解を世界に向けて公表する予定です。
☑発表会のアーカイブについて
3月31日に東京都内で開催された本件の発表会のアーカイブは以下の配信サイトにてご覧いただけます。また、LANAプロジェクト中心メンバーから寄せられたコメントは、発表会アーカイブのほかZMCホームページにてご覧いただけます。

【発表会アーカイブ】
•
YouTube：https://www.youtube.com/live/b9ZV-4T3iUo
•
ニコニコ生放送：https://live.nicovideo.jp/watch/lv350105847
 
❙ ZMC（ZEN Mathematics Center; ZEN数学センター）とは
ZMCは、数論幾何学を中心とした現代数学や、コンピューター言語を用いた現代数学の形式化
（formalization）の推進と発展を目指して設立された国際研究所です。
ZMCホームページ▶ https://zen.ac.jp/zmc
 
❙ ZEN大学について
　ZEN大学は、最先端のIT技術を活用し、すべての人に大学進学の機会を提供します。ZEN大学唯一の学部である「知能情報社会学部」では、特定の学問領域に偏らない学びを修めることで、激変するAI時代に対応して活躍するために必要なリテラシーを身につけることができます。
 
　2025年7月23日（水）より、2025年10月入学生の出願受付を開始します。また、2025年9月2日（火）からは2026年4月入学生の出願受付を開始します。ZEN大学では学ぶ意欲のある方々に対して広く高等教育の機会を提供するため、入学選考において学力試験は行いません。志望理由・小論文により選考します。
　
さらに詳しい情報は、ZEN大学のウェブサイトおよびパンフレットをご覧ください。
ZEN大学に関する詳細▶ https://zen.ac.jp/
最新パンフレット請求▶ https://zen.ac.jp/form