For the LANA Project Announcement

We are pleased to present comments from the following individuals on the occasion of the LANA Project announcement held on March 31, 2026.

Masato Wakayama (President of ZEN University)

Thank you very much for taking the time out of your busy schedules to join us today for the announcement of the "LANA Project" by our ZEN Mathematics Center (ZMC). As we enter the era of AI, the efficacy and expanding potential of computer-assisted proofs in pure mathematics are becoming a tangible reality. Today, I am pleased to share with you this initiative by ZMC. While the project's name is derived from the proof assistant Lean and anabelian geometry—a subfield of arithmetic geometry—Professor Fumiharu Kato, Director of ZMC and leader of this project, will elaborate on the technical details shortly. For my part, I would like to explain the context and the reasons behind today’s announcement.

ZEN University was established in April last year as a fully-fledged online university, with a resolute mission to alleviate and resolve the severe educational disparities in Japan. By leveraging the latest IT technologies, such as the Internet and Artificial Intelligence, we aim to forge a new paradigm of higher education that has been difficult to realize within traditional university frameworks. At the same time, as an institution of higher learning, academic research—which fundamentally supports education and enriches the intellectual heritage of humanity—remains one of our vital pillars. At ZEN University, we are systematically advancing research on several themes that have received limited attention from conventional universities in Japan. The LANA Project by ZMC is a prime example of this endeavor.

Historically, the use of Lean was not widespread in mathematical research. However, with the dramatic increase in computational power and the emerging potential of automated theorem proving through AI, it has now taken center stage. Lean itself is a general-purpose programming language as well as an interactive theorem prover, and it is not inherently tied to AI. The reason it is often discussed alongside AI is the opportunity for automated formalization—the process of translating natural language and mathematical equations used by humans into computer code. In fields with a long history and well-established theoretical frameworks, where vast amounts of research and methodologies have accumulated, there are high hopes for this automated formalization in part.

Looking abroad, initiatives to advance modern mathematics through Lean formalization are being spearheaded by prominent figures, including Fields Medalist Terence Tao. Recently, I attended part of a conference on "AI and Mathematics" at the Institute for Mathematical Sciences at the National University of Singapore. There, I encountered a fascinating report on a  team-based research achieving Lean formalization in the fields of representation theory and number theory, involving problems such as the Kazhdan-Lusztig conjecture and affine Deligne-Lusztig varieties. I believe this will become a major tide in mathematical research. While individual attempts using Lean are likely being made across Japan, we have yet to see a concerted, organized, and full-scale institutional effort. Recognizing this landscape, we made the decision to advance the LANA Project.

The project has two primary objectives. The first is to formalize the major theorems of anabelian geometry—a field to which Japanese mathematicians have made outstanding contributions—using Lean, and to construct a library for it. The second is the verification of Inter-Universal Teichmüller (IUT) theory, developed by Professor Shinichi Mochizuki of Research Institute for Mathematical Sciences at Kyoto University, through Lean formalization. This theory has yet to reach a consensus among the global mathematical community. Therefore, its verification itself will be of profound significance for the advancement of mathematics. Led by Professor Kato, we have successfully assembled an unparalleled international team to achieve these objectives. Though focused on a specific domain, it is arguably the finest team in the world for this purpose.

This represents a bold new frontier for our university. Thank you very much for your time and support today.

Fumiharu Kato (Director of the ZMC)

Thank you all very much for gathering here today.

At today's press conference, we would like to formally announce to all of you that we have launched a new "LANA Project." Until today, we have not disclosed anything at all about this LANA Project, including even its existence. In fact, however, if one includes the preparation period, this project has already been underway since the autumn of 2023. Since the project began operating in earnest in September 2024, this means that we have already been active for more than a year and a half.

First of all, I would like to speak about the aims of LANA, that is, "Lean for ANAbelian geometry." Broadly speaking, this project has two aims.

The first aim is the formalization of anabelian geometry and the construction of its library. "Anabelian geometry" is an important field of arithmetic geometry in which Japanese researchers have long played a particularly prominent role. In the LANA Project, we aim to formalize the principal theorems of this anabelian geometry and their proofs by using the computer proof assistant Lean, and to build its library. At the same time, in order to encourage the spread of Lean and the formation of a community within the Japanese mathematical world, we will organize various events, including research meetings.

The second aim is to verify inter-universal Teichmüller theory, the so-called IUT theory, due to Professor Shinichi Mochizuki of the Research Institute for Mathematical Sciences, Kyoto University, likewise by means of Lean formalization. Without leaning toward any particular position, we aim, from a neutral point of view, to put this theory into a form that can be formalized and, by verifying it, to bring to an end the controversy surrounding this theory that has continued for many years.

In order to achieve these goals, we have assembled a powerful group of members from all over the world for this project. For my part, I take pride in the fact that these members are truly the best in the world for accomplishing these goals.

Next, let me introduce the core members of the LANA Project. There are five core members. They are Johan Commelin of Utrecht University, Kiran Kedlaya of the University of California, San Diego, Yuichiro Hoshi of the Research Institute for Mathematical Sciences, Kyoto University, Adam Topaz of the University of Alberta, and myself, Fumiharu Kato, the project leader. In addition to these core members, around seven younger members, including students and postdocs, are also participating. On this occasion, Messrs. Commelin, Kedlaya, and Topaz are participating in this event online, and they will each give a speech later. Yuichiro Hoshi is absent on other business, but he has sent us a message, which I will read aloud later.

There is one point I would like to mention regarding the achievements of these members. In December 2020, there began a formalization project in contemporary mathematics called the Liquid Tensor Experiment, which started from a challenge posed by Fields Medalist Peter Scholze—who is also famous for publicly expressing a negative view of IUT theory—and in July 2022, just a year and a half after Scholze's challenge, it was completed in Lean. This event also became an opportunity to demonstrate to the world the power of Lean formalization. In fact, the team that completed this Liquid Tensor Experiment was led, by none other than Johan Commelin and Adam Topaz of this project, as its leaders. In truth, I was deeply struck by this event, and that led me to conceive the LANA Project.

Here, let me briefly explain the formalization of mathematics by Lean. Lean is one of the functional programming languages known as proof assistants. When one hears the term "proof assistant," one may imagine something that proves mathematical theorems on behalf of human beings, but in fact that is not what it is. Ordinarily, mathematical arguments are written by using natural language, such as Japanese or English, together with mathematical formulas. By contrast, formalization using a proof assistant such as Lean means rewriting such mathematical arguments in a programming language. In other words, it is a translation from natural language into formal language. In order to do this, one must eliminate as much as possible the ambiguity that natural language possesses and fill in the omitted intermediate steps. Therefore, formalization may be said to be the work of arranging the line of a mathematical argument into a form that is more rigorous and easier to share.

However, IUT theory is a vast and complex theory, and moreover, even at present the world's mathematicians are divided in their opinions concerning whether it is correct. Therefore, the work of formalizing it cannot be carried out merely by a mechanical translation—assuming that such a thing were possible. We ourselves, in carrying out the work, must attain a sufficiently deep understanding of IUT theory. For that reason, in the LANA Project, we have spent more than a year engaged in intensive discussions about IUT theory. We have held bootcamps in various places, including Japan, Canada, the Netherlands, and the United States; read papers and various other materials; organized the points at issue; and built the foundation for verification by comparing our understandings with one another.

As a result, we take pride in the fact that we have now come to share among the members a considerably deep understanding of IUT theory. Because of that, we have become able to state clearly how far we truly understand things, and what remains unresolved and in what way. What is important is that we have become able to express, in plain mathematical language, those points that still have not been clarified.

What must be stated carefully here is that, at the present stage, we have not yet reached a final conclusion as to whether those points constitute mathematical gaps or whether they derive from limitations in our own understanding. Mathematics is an objective discipline, and to speak in a way faithful to that objectivity, there is of course, at least as a possibility, the possibility that there are defects in the argument at those points. Therefore, this point is precisely the central issue going forward, and we intend to continue examining it from an entirely neutral standpoint and also to continue our dialogue with Professor Mochizuki.

Let me now speak about our future outlook. On July 17 of this year, we plan to present to the world, in the form of a press conference, an interim report on the activities of the LANA Project. On that occasion, with regard to the verification of IUT theory, we intend to organize and present the details of our understanding up to that point. This will include not only the points that we have understood, but also the points that we have not yet understood, as well as how we are articulating and positioning them. In other words, by the press conference on July 17, we intend to compile these issues and the verification results at that point as an interim report and present them to the world.

We believe that, by pursuing in parallel a deep understanding of mathematics and rigorous confirmation by computer, we can open up a new horizon in mathematical research. The LANA Project is a challenge undertaken for that purpose. We intend to continue facing this task sincerely and tenaciously.

Next, from this point onward, the participants joining online will give their speeches. First, Johan Commelin will speak about the significance of Lean formalization in future mathematical research and the need to build a community in Japan. Next, Adam Topaz will comment on the possibility that Lean may greatly change the way mathematical research is conducted, as well as on the current state and outlook of our research concerning IUT theory. Kiran Kedlaya will speak about his own involvement with IUT theory and the impact that the formalization of mathematics by computer may have on the future of mathematics.

With that, I will conclude my remarks here. Thank you very much for your attention.

Johan Commelin (Utrecht)

I am grateful for the opportunity to add a few words to what has already been said. As mentioned by professor Kato before, Adam Topaz and I have led the Liquid Tensor Experiment. After the successful completion of that project, people asked me if I thought Lean should be used to verify IUT theory. My response was: only if people from the Japanese community, people with expertise in IUT, would be involved. You can imagine my excitement when I was contacted by professor Kato, proposing to launch the LANA project.

Firstly, I am glad to collaborate with ZMC on building a formalization/Lean community within the Japanese math community. I believe that mathematics is a conversation between informal intuition and formal rigour. Lean and mechanization of mathematics play an increasing role in this dialogue. I am proud to collaborate with ZMC on spearheading this effort during our bootcamps and conferences.

Secondly, as part of the LANA project, we are building out the foundations of anabelian geometry in Lean. For example, the theory of Galois categories and fundamental groups.We are now seeing foundational parts of algebraic, arithmetic, and anabelian geometry contributed to the Mathlib library. It is a solid foundation to build other projects of formal mathematics on top of.

Finally, using Lean, we can make the claims and arguments in IUT absolutely precise and rigorous. It is essential for our project to distinguish between formal verification and generative AI prediction. Generative AI synthesizes text based on statistical patterns and can hallucinate. In contrast, Lean validates mathematical truth against strict logical rules. This removes the ambiguity that often occurs in informal presentations of mathematics. A proof verified in Lean gives a guarantee of correctness that is impossible to achieve with the traditional peer review process.

I am thrilled about these new developments in mathematics, both in the context of the LANA project and in general. I thank Kawakami-san and ZMC for supporting this important project, and I am excited about our continued collaboration.

Adam Topaz (Alberta)

I am in a somewhat unusual position among mathematicians in that my research spans both sides of this project. I work in anabelian geometry, and I am also deeply involved in formal verification using Lean. Having worked seriously in both, I have experienced firsthand how formalization changes the way you think about mathematics. I believe this goes to the heart of why this project exists.

Mathematics has been done in the same way for thousands of years. We write arguments in natural language, share them with colleagues, and form judgments about whether they are correct. But formalization asks us to go further. It forces us to be completely explicit and precise, but it also forces us to rethink and optimize the mathematical concepts we use. The formalization process still requires human effort and creativity. What a proof assistant does is check the internal logical consistency. Whether the definitions and statements have been formalized correctly is still something only human mathematicians can answer.

When a mathematical theory is sufficiently vast and sufficiently contested, the traditional informal processes of verification can break down. Reasonable mathematicians, reading carefully and in good faith, can reach vastly different conclusions. Formalization provides a framework where such points of contention can be examined unambiguously.

That is precisely the spirit in which we have approached IUT. Over the past year and a half, our team has invested enormous effort in building a deep, shared understanding of IUT theory, always with formalization in mind. There is a specific point in the theory that we have encountered repeatedly throughout the project. We have approached it from multiple directions, each time with deeper understanding. We have now reached a stage where we can articulate this point with enough precision to be able to formalize it in Lean, but we have been unable to proceed beyond this point. Whether this reflects a genuine gap in the proof, or the boundaries of our own current understanding of IUT, we are not yet in a position to say definitively.

I want to reiterate what Professor Kato said: we intend to continue our examination of this point and our dialogue with Professor Mochizuki. We believe that the precision provided by Lean will make that dialogue more productive and transparent than has previously been possible. The mathematical community deserves unambiguous clarity on this issue, and we are committed to pursuing it with honesty and rigor.

Finally, let me say that I am deeply grateful to Mr. Kawakami, Professor Kato and ZMC for assembling and supporting this team with such seriousness of purpose. I am proud to be part of this project, and I look forward to sharing our progress with the world.

Thank you.

Kiran Kedlaya (UCSD)

While I am a newcomer to mathematical formalization, my interest in IUT long predates the LANA project. In 2015, Oxford University hosted a workshop where many arithmetic geometers with no prior exposure to IUT made a concerted effort to digest the subject, including reading and presenting earlier papers of Mochizuki. While that workshop did not lead to a breakthrough in community understanding of IUT, it did prove very enlightening.

Unfortunately, community efforts to process IUT subsequently stalled due to slow progress plus a widespread belief that the 2018 manuscript of Scholze--Stix identified a fundamental logical inconsistency in IUT. While I also limited my study of IUT in this time, I remained in occasional contact with some experts, attended some additional meetings on the subject, and ascertained that the appearance of inconsistency had been caused by a miscommunication. I thus considered the status of IUT to be still unresolved.

I joined the LANA project both to get caught up on the formalization revolution and to help build consensus on the status of IUT and the ABC conjecture. Should the project reach a positive conclusion about IUT, I am prepared to expend social capital to bring this conclusion forward to mainstream researchers in arithmetic geometry.

One early learning for me is Adam's point that formalization goes well beyond software. It is also a matter of sociology: in order to use new tools to construct correct mathematics, we must also consider how mathematicians reach consensus about correctness. As the proofs of influential theorems have become increasingly complex, verification has relied on a fragile web of trust among mathematicians; while artificial intelligence shows great promise to tame the complexity, the unreliable nature of large language models brings the risk of damaging that fragile trust. The LANA project represents a path forward, in which the focus remains on promoting human understanding with the help of sophisticated software tools. I look forward to the continuing work of the project team in the coming months and thank Professor Kato and ZMC for making this work possible.

Yuichiro Hoshi (Research Institute for Mathematical Sciences, Kyoto University)

I have joined the LANA Project in 2024 as one of the core members and have been working with the other members ever since.  Looking back, I feel that this more than a year in the project was a period in which I have continuously confronted the question of how to explain inter-universal Teichmuller theory should be explained. 

The role that I myself have undertaken in the LANA project has been to explain the content of inter-universal Teichmuller theory to the members of the project as comprehensively as possible.  On particularly important points, I have tried to give explanations as carefully as possible and with as much time as necessary, so that we could share not merely an outline-level understanding but also the details of the logic.  In particular, one major goal toward which I have been working has been to establish a understanding, among the members of the project, of the logic by which Corollary 3.12 is derived from Theorem 3.11 of the third paper of the inter-universal Teichmuller theory published in 2021. 

To that end, we have spent a great deal of time holding discussions, repeating explanations, and organizing the issues from as many angles as possible.  As a result, through these efforts over the past year and more, I am confident that the members' understanding of inter-universal Teichmuller theory has certainly advanced greatly.  At the very least, I do not think that there are many people outside of those directly involved with inter-universal Teichmuller theory who have tried to understand it this seriously and worked on it this persistently.  In that sense, I feel that this project is of great significance, and, moreover, I am very happy to be participating in such a project.

At the same time, however, I also believe, regrettably, that I have not yet fully fulfilled my role.  In particular, with regard to the logic by which Corollary 3.12 is derived from Theorem 3.11 as I mentioned earlier, I must take seriously the fact that many members of the LANA Project still feel that there is some insurmountable wall there.  Then I also keenly feel my own shortcomings in the face of such a situation. 

Nevertheless, I do not think at all that the efforts we have made over the past year and more have been meaningless.  On the contrary, I think that precisely because we have thought so seriously, discussed so extensively, and tried so hard to understand matters up to this point, it has become far clearer than before where the true difficulty really lies.  In that sense as well, I believe that the efforts we have made on this project have definite value and significance. 

Finally, I would like to express my deep gratitude to the ZEN Mathematics Center and Professor Fumiharu Kato.  There can be no doubt that this meaningful undertaking could never have been possible without the many forms of substantial support and devoted effort that they have provided up to now.  Thank you very much. 

Going forward as well, while continuing to face the remaining issues sincerely, I would like to keep making efforts to improve the understanding of the members of the project as much as possible.  Thank you very much.