ZEN數學中心發布新專案「LANA」，旨在透過電腦驗證宇宙際Teichmüller（IUT）理論

ZEN大學的「ZMC（ZEN Mathematics Center:ZEN數學中心）」於2026年3月31日（星期二）宣布啟動新專案「LANA」。LANA是一個以ZEN大學（日本）、烏特勒支大學（荷蘭）和亞伯達大學（加拿大）為中心的國際合作研究專案，主要目標是形式化算術幾何學中的重要領域——遠阿貝爾幾何學，並驗證京都大學數理解析研究所望月新一教授提出的宇宙際Teichmüller理論（IUT理論）。

該專案自2023年秋季（包括準備期）以來一直在幕後運作。在3月31日於東京都舉行的發布會上，LANA專案的成立背景、目標、基本方針、核心成員、目前活動狀況以及未來展望首次公開。

☑︎關於LANA專案

LANA是「Lean for ANAbelian geometry」的縮寫。專案的第一個目標是利用證明輔助系統Lean，將日本研究人員引領世界的算術幾何學重要領域——遠阿貝爾幾何學的主要定理形式化，並建立其函式庫。第二個目標是利用Lean形式化IUT理論並進行驗證。

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（加州大學聖地牙哥分校教授）