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