ZEN Mathematics Center Announces New Project "LANA" Aiming for Computer Verification of Inter-Universal Teichmüller (IUT) Theory

ZEN University's "ZMC (ZEN Mathematics Center)" announced on Tuesday, March 31, 2026, a new project called "LANA." LANA is an international collaborative research project centered around ZEN University (Japan), Utrecht University (Netherlands), and the University of Alberta (Canada). Its main objectives are the formalization of anabelian geometry, a crucial field in arithmetic geometry, and the verification of Inter-Universal Teichmüller Theory (IUT theory) by Professor Shinichi Mochizuki of the Research Institute for Mathematical Sciences, Kyoto University.

This project has been active behind the scenes since the autumn of 2023, including its preparation period. At the announcement event held in Tokyo on March 31, the background, objectives, basic policy, core members, current activities, and future outlook of the LANA project were publicly revealed for the first time.

☑︎About the LANA Project

LANA stands for "Lean for ANAbelian geometry." The first objective of the project is to formalize the main theorems of anabelian geometry, a significant field in arithmetic geometry where Japanese researchers have led the world, using the proof assistant Lean, and to build its library. The second objective is to formalize IUT theory using Lean and to verify it.

Lean is a functional programming language and does not automatically prove mathematical theorems by itself. To formalize mathematical arguments, which are usually described in natural languages like Japanese or English and mathematical formulas, into Lean's language, it is necessary to rewrite them while eliminating ambiguity as much as possible. Especially for a vast and complex theory like IUT theory, this work is not merely a mechanical conversion but requires a deep specialized understanding of the theory itself.

The LANA project aims to prepare IUT theory in a formalizable form and verify it, maintaining a neutral perspective without bias towards any particular stance. At a time when mathematicians' opinions are still divided over the validity of the theory, clarifying the points of contention and presenting them in a shareable form is a crucial significance of this project.

☑︎Background of Formation

The concept behind the LANA project is rooted in the significant advancements in mathematical formalization in recent years. In particular, the "Liquid Tensor Experiment," initiated by the proposal of Fields Medalist Peter Scholze, was a symbolic example demonstrating that highly advanced arguments in modern mathematics could actually be verified using Lean. Johan Commelin, an assistant professor at Utrecht University, and Adam Topaz, who led this project, are also core members of the current LANA project.

Following these precedents, ZMC has been exploring the possibility of engaging with important theories in modern mathematics in new ways through formalization. The LANA project, as an international collaborative research effort, was launched as a result.

☑︎LANA Project Core Members

Fumiharu Kato (Professor at ZEN University, Emeritus Professor at Tokyo Institute of Science, Project Leader)

Johan Commelin (Assistant Professor at Utrecht University)

Kiran Kedlaya (Professor at University of California, San Diego)