ZEN数学センターは2026年3月31日、新プロジェクト「LANA（Lean for ANAbelian geometry）」を発表した。日本、オランダ、カナダの大学が連携する国際共同研究として、数論幾何学の重要分野である遠アーベル幾何学の形式化と、宇宙際タイヒミューラー理論の検証を目指す。

　同プロジェクトには、ZEN大学、ユトレヒト大学、アルバータ大学を中心に研究者が参加。2023年秋から準備を進めており、東京都内で開催された発表会で概要が公表された。

　LANAでは、証明支援系プログラミング言語Leanを用い、数学理論を形式的に記述・検証する。特に、京都大学数理解析研究所の望月新一教授が提唱したIUT理論について、曖昧さを排除した形で再構成し、検証可能な形に整理することを目的とする。

　IUT理論は、その複雑さと独自性から国際的にも評価が分かれており、数学界で議論が続いている。LANAプロジェクトは特定の立場に偏らず中立的な視点を保ちつつ、論点の明確化と共有を図る方針だ。

　プロジェクトの中心メンバーには、加藤文元氏（ZEN大学教授）、ヨハン・コメリン氏（ユトレヒト大学）、キラン・ケドラヤ氏（カリフォルニア大学サンディエゴ校）、星裕一郎氏（京都大学）、アダム・トパーズ氏（アルバータ大学）らが名を連ねる。若手研究者も含めた国際的な体制で研究を進めている。

　同センターによると、これまでの研究活動を通じて、IUT理論の理解が及んでいる範囲と未解明の論点が徐々に明確になってきたという。2026年7月17日には中間報告を公表し、検証の進捗や現時点での見解を発表する予定としている。

　近年、数学における形式化研究は進展しており、証明支援系を用いた大規模理論の検証が現実的な手法として注目されている。LANAプロジェクトは、こうした潮流の中で最先端理論の検証に挑む取り組みとして位置付けられる。