ZEN Mathematics Center Announces New Project "LANA" Aiming for Computer-Aided Verification of IUT (Inter-universal Teichmüller) Theory
ZEN Mathematics Center launches "LANA," an international collaborative research project with three global universities, to formalize anabelian geometry and verify IUT Theory using computers.
📋 Article Processing Timeline
- 📰 Published: March 31, 2026 at 23:00
ZEN University's "ZMC (ZEN Mathematics Center)" announced a new project called "LANA" on Tuesday, March 31, 2026. 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 number theory and 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.
Including its preparation period, this project has been active behind the scenes since the autumn of 2023. At the press conference held in Tokyo on March 31, the background, objectives, basic policy, core members, current activity status, and future outlook of the LANA project were publicly announced for the first time.
**About the LANA Project**
LANA is an acronym for "Lean for ANAbelian geometry." The first objective of the project is to formalize the main theorems of anabelian geometry, a significant field in number theory and 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, typically 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 task is not merely a mechanical conversion but requires a deep specialized understanding of the theory itself.
The LANA project aims to organize IUT Theory into a formalizable form and verify it, maintaining a neutral perspective without bias towards any particular stance. In a situation where mathematicians' opinions are still divided regarding the validity of the theory, clarifying the points of contention and presenting them in a shareable format is a significant meaning of this project.
**Background of Formation**
The concept behind the LANA project is rooted in the significant advancements in the formalization of mathematics in recent years. In particular, the "Liquid Tensor Experiment," initiated by Fields Medalist Peter Scholze, was an emblematic case that demonstrated how advanced discussions in modern mathematics could actually be verified using Lean. Johan Commelin 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 a new way through formalization. The LANA project, as an international collaborative research effort, was launched as a result.
**LANA Project Core Members**
Fumiharu Kato (Professor, ZEN University; Professor Emeritus, Tokyo Institute of Technology; Project Leader)
Johan Commelin (Assistant Professor, Utrecht University)
Kiran Kedlaya (Professor, University of California San Diego)
Yuichiro Hoshi (Associate Professor, Research Institute for Mathematical Sciences, Kyoto University)
Adam Topaz (Associate Professor, University of Alberta)
In addition, about seven young members, including students and postdoctoral researchers (from three countries/regions), are participating, advancing activities under an international and multi-layered research system.
**Current Status and Future Outlook of IUT Theory Verification**
For over a year, the LANA project has been working on understanding and verifying IUT Theory through numerous camps and intensive workshops held in various locations including Japan, Canada, the Netherlands, and the United States. As a result, it has become quite clear to what extent the research team currently understands the theory, and which points remain beyond their comprehension. Furthermore, efforts are underway to organize the points that are not yet understood into the plainest possible mathematical language.
An interim report press conference regarding the LANA project is scheduled for Friday, July 17, 2026. The plan is to publicly announce the verification results of IUT Theory in detail at that time.
**Comments**
**Masato Wakayama (President, ZEN University)**
ZEN University opened in April last year with the aim of alleviating and resolving the serious educational disparities in Japan by creating a full-fledged online university. By utilizing the latest IT technologies such as the internet and AI, we aim to create a new form of university education that was difficult to achieve with existing universities.
On the other hand, as long as it is a university, research that supports education from the ground up and enriches humanity's intellectual property is also a major pillar. At our university, we are systematically advancing research on several themes that existing universities have not actively pursued. The international project "LANA" of the ZEN Mathematics Center in cutting-edge mathematics, based on the dramatic progress in computer computational power, is one such initiative and is positioned as a new challenge for our university.
**Fumiharu Kato (Professor, ZEN University / Director, ZMC, LANA Project Leader)**
The LANA project is an international collaborative research that tackles the forefront of modern mathematics, anabelian geometry and IUT Theory, with a new approach: formalization using the proof assistant Lean. IUT Theory is vast and complex, and mathematicians worldwide are still divided on its validity. We have assembled the best staff and have been discussing this theory for over a year. As a result, we believe it has become quite clear to what extent our understanding extends at present, and which points remain unexplained. However, we have not yet concluded whether these are truly mathematical gaps or issues with our own understanding. Therefore, we intend to continue our examination from a neutral standpoint and advance dialogue with Professor Mochizuki. In the interim report on July 17, we plan to publicly announce our understanding up to that point to the world.
**About the Archive of the Press Conference**
The archive of the press conference held in Tokyo on March 31 can be viewed on the following distribution sites. Comments from the core members of the LANA project can also be found on the ZMC website in addition to the press conference archive.
**[Press Conference Archive]**
* YouTube: https://www.youtube.com/live/b9ZV-4T3iUo
* Nico Nico Live: https://live.nicovideo.jp/watch/lv350105847
**About ZMC (ZEN Mathematics Center)**
ZMC is an international research institute established with the aim of promoting and developing modern mathematics, particularly number theory and geometry, and the formalization of modern mathematics using computer languages.
ZMC Website: https://zen.ac.jp/zmc
**About ZEN University**
ZEN University utilizes cutting-edge IT technology to provide university admission opportunities to everyone. In the "Faculty of Intelligent Information Society," the only faculty at ZEN University, students can acquire the literacy necessary to thrive in the rapidly changing AI era by pursuing studies not biased towards specific academic fields.
Applications for October 2025 enrollment will begin on Wednesday, July 23, 2025. Additionally, applications for April 2026 enrollment will begin on Tuesday, September 2, 2025. ZEN University does not conduct academic achievement tests for admission selection to widely provide higher education opportunities to those with a desire to learn. Selection is based on reasons for application and essays.
For more detailed information, please visit the ZEN University website and brochure.
ZEN University Details: https://zen.ac.jp/
Request Latest Brochure: https://zen.ac.jp/form
Including its preparation period, this project has been active behind the scenes since the autumn of 2023. At the press conference held in Tokyo on March 31, the background, objectives, basic policy, core members, current activity status, and future outlook of the LANA project were publicly announced for the first time.
**About the LANA Project**
LANA is an acronym for "Lean for ANAbelian geometry." The first objective of the project is to formalize the main theorems of anabelian geometry, a significant field in number theory and 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, typically 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 task is not merely a mechanical conversion but requires a deep specialized understanding of the theory itself.
The LANA project aims to organize IUT Theory into a formalizable form and verify it, maintaining a neutral perspective without bias towards any particular stance. In a situation where mathematicians' opinions are still divided regarding the validity of the theory, clarifying the points of contention and presenting them in a shareable format is a significant meaning of this project.
**Background of Formation**
The concept behind the LANA project is rooted in the significant advancements in the formalization of mathematics in recent years. In particular, the "Liquid Tensor Experiment," initiated by Fields Medalist Peter Scholze, was an emblematic case that demonstrated how advanced discussions in modern mathematics could actually be verified using Lean. Johan Commelin 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 a new way through formalization. The LANA project, as an international collaborative research effort, was launched as a result.
**LANA Project Core Members**
Fumiharu Kato (Professor, ZEN University; Professor Emeritus, Tokyo Institute of Technology; Project Leader)
Johan Commelin (Assistant Professor, Utrecht University)
Kiran Kedlaya (Professor, University of California San Diego)
Yuichiro Hoshi (Associate Professor, Research Institute for Mathematical Sciences, Kyoto University)
Adam Topaz (Associate Professor, University of Alberta)
In addition, about seven young members, including students and postdoctoral researchers (from three countries/regions), are participating, advancing activities under an international and multi-layered research system.
**Current Status and Future Outlook of IUT Theory Verification**
For over a year, the LANA project has been working on understanding and verifying IUT Theory through numerous camps and intensive workshops held in various locations including Japan, Canada, the Netherlands, and the United States. As a result, it has become quite clear to what extent the research team currently understands the theory, and which points remain beyond their comprehension. Furthermore, efforts are underway to organize the points that are not yet understood into the plainest possible mathematical language.
An interim report press conference regarding the LANA project is scheduled for Friday, July 17, 2026. The plan is to publicly announce the verification results of IUT Theory in detail at that time.
**Comments**
**Masato Wakayama (President, ZEN University)**
ZEN University opened in April last year with the aim of alleviating and resolving the serious educational disparities in Japan by creating a full-fledged online university. By utilizing the latest IT technologies such as the internet and AI, we aim to create a new form of university education that was difficult to achieve with existing universities.
On the other hand, as long as it is a university, research that supports education from the ground up and enriches humanity's intellectual property is also a major pillar. At our university, we are systematically advancing research on several themes that existing universities have not actively pursued. The international project "LANA" of the ZEN Mathematics Center in cutting-edge mathematics, based on the dramatic progress in computer computational power, is one such initiative and is positioned as a new challenge for our university.
**Fumiharu Kato (Professor, ZEN University / Director, ZMC, LANA Project Leader)**
The LANA project is an international collaborative research that tackles the forefront of modern mathematics, anabelian geometry and IUT Theory, with a new approach: formalization using the proof assistant Lean. IUT Theory is vast and complex, and mathematicians worldwide are still divided on its validity. We have assembled the best staff and have been discussing this theory for over a year. As a result, we believe it has become quite clear to what extent our understanding extends at present, and which points remain unexplained. However, we have not yet concluded whether these are truly mathematical gaps or issues with our own understanding. Therefore, we intend to continue our examination from a neutral standpoint and advance dialogue with Professor Mochizuki. In the interim report on July 17, we plan to publicly announce our understanding up to that point to the world.
**About the Archive of the Press Conference**
The archive of the press conference held in Tokyo on March 31 can be viewed on the following distribution sites. Comments from the core members of the LANA project can also be found on the ZMC website in addition to the press conference archive.
**[Press Conference Archive]**
* YouTube: https://www.youtube.com/live/b9ZV-4T3iUo
* Nico Nico Live: https://live.nicovideo.jp/watch/lv350105847
**About ZMC (ZEN Mathematics Center)**
ZMC is an international research institute established with the aim of promoting and developing modern mathematics, particularly number theory and geometry, and the formalization of modern mathematics using computer languages.
ZMC Website: https://zen.ac.jp/zmc
**About ZEN University**
ZEN University utilizes cutting-edge IT technology to provide university admission opportunities to everyone. In the "Faculty of Intelligent Information Society," the only faculty at ZEN University, students can acquire the literacy necessary to thrive in the rapidly changing AI era by pursuing studies not biased towards specific academic fields.
Applications for October 2025 enrollment will begin on Wednesday, July 23, 2025. Additionally, applications for April 2026 enrollment will begin on Tuesday, September 2, 2025. ZEN University does not conduct academic achievement tests for admission selection to widely provide higher education opportunities to those with a desire to learn. Selection is based on reasons for application and essays.
For more detailed information, please visit the ZEN University website and brochure.
ZEN University Details: https://zen.ac.jp/
Request Latest Brochure: https://zen.ac.jp/form
FAQ
What are the main objectives of the LANA project?
The formalization of anabelian geometry and the computer-aided verification of Professor Shinichi Mochizuki's Inter-universal Teichmüller Theory (IUT Theory).
What is IUT Theory?
It is a theory in number theory and geometry proposed by Professor Shinichi Mochizuki of Kyoto University, believed to be related to the proof of the ABC conjecture, but its validity is still debated among mathematicians.
What kind of tool is Lean?
Lean is a proof assistant (functional programming language) used to formally describe mathematical theorems and proofs, and to verify their correctness using a computer.