ZEN大学「ZMC（ZEN Mathematics Center; ZEN数学センター）」新プロジェクト「LANA」の発表
- Date: March 31, 2026
- Video: https://www.youtube.com/live/b9ZV-4T3iUo
- Duration: 1h 24m (first ~11 minutes are pre-stream holding screen)
- Language: Japanese (with some English from online participants, consecutively translated)
ZEN University's ZEN Mathematics Center (ZMC) publicly announced the LANA project (Lean + ANabelian geometry), a formalization effort that has been running secretly since fall 2023 (full operation from September 2024). The project has two goals:
- Formalize the main theorems of anabelian geometry in Lean and build a library, while promoting Lean adoption in Japan
- Verify Mochizuki Shinichi's Inter-universal Teichmüller (IUT) theory through Lean formalization, from a neutral standpoint
- Johan Commelin (Utrecht University) — Mathlib initiative director, Liquid Tensor Experiment co-leader
- Kiran Kedlaya (UC San Diego) — p-adic Hodge theory / p-adic differential equations expert
- Hoshi Yuichiro (RIMS, Kyoto University) — anabelian geometry, close collaborator of Mochizuki
- Adam Topaz (University of Alberta) — Mathlib initiative senior manager, Liquid Tensor Experiment co-leader
- Katō Fumiharu (ZEN University) — project leader, ZMC director
Plus ~7 junior members (students/postdocs).
After 1.5+ years of intensive study (boot camps in Japan, Canada, Netherlands, USA), the team reports:
- They can now articulate in plain mathematical language what they understand and what remains unresolved about IUT
- There is a specific point in the derivation of Corollary 3.12 from Theorem 3.11 in IUT Paper III where they cannot yet proceed
- They have not reached a final conclusion on whether this represents a mathematical gap in the proof or a limitation of their own understanding
- They acknowledge that the possibility of a deficiency in the argument exists
- They have communicated this to Mochizuki and will continue dialogue
- Commelin and Topaz confirmed they can express the problematic point with enough precision to formalize in Lean, but cannot yet go further
- Hoshi (the member closest to IUT) stated that many LANA members feel there is an "insurmountable wall" at this point, and he takes this seriously
A press conference is scheduled for July 17, 2026 to present a detailed interim report, including:
- What they understand about IUT
- What remains unresolved
- How they've formalized and positioned the key questions
The full project is expected to take at least several years.
- Relationship with Mochizuki: The project maintains near-complete independence. They are "questioners" only. Communication is in writing. Mochizuki's October 2025 report included a positive section on Lean formalization.
- On Scholze's objection: Katō declined to comment, deferring to the July 17 press conference.
- On AI: AI will not be used for the critical 3.11→3.12 part (human hands only). AI may assist with foundational building blocks.
- Comparison with Liquid Tensor Experiment: Commelin said the Lean formalization challenges in LTE were "at least as hard" as in LANA. The mathematical challenges differ in nature.
- Kedlaya on consensus: If LANA reaches a positive conclusion on IUT, he intends to use his "social capital" to disseminate the conclusion among mainstream arithmetic geometry researchers. He considers IUT's status "still unresolved."
- Anabelian geometry contributions: Foundational parts (Galois theory, fundamental groups) are already being contributed to Mathlib.
Translated from auto-generated Japanese transcript (mlx-whisper, large-v3-turbo). Lines marked [EN] are where the original English audio was captured by Whisper. The online speakers (Commelin, Topaz, Kedlaya) spoke in English with consecutive Japanese interpretation; Whisper mostly captured the interpreter's Japanese version.
[10:49] Thank you for coming to the announcement of our university's ZEN Mathematics Center LANA Project. Now that we have entered the AI era, the effectiveness and expanding possibilities of computer-assisted proof in essential areas of pure mathematics are becoming a reality. Today I would like to report on this ZMC project.
[11:17] The project name is based on the proof assistant Lean and anabelian geometry, a subfield of arithmetic geometry. Details will be presented later by Professor Katō Fumiharu, who serves as ZMC director and leads this project.
[11:33] I would like to explain why we are making this announcement today. Our university was established last April to create a full-fledged online university and address Japan's serious educational disparity.
[11:47] We opened last April to help alleviate this gap. By leveraging the latest IT technologies including the internet and AI, we aim to create new forms of education that were difficult to achieve at existing universities.
[12:01] At the same time, as long as we are a university, academic research that fundamentally supports education and enriches humanity's intellectual heritage is also a major pillar.
[12:14] ZEN University is systematically advancing research on several themes that existing universities have not much pursued. One of these is the LANA Project by ZMC, which we introduce today.
[12:26] In mathematics, research using Lean was not previously very active. However, with the dramatic improvement in computational power
[12:37] and the emerging possibility of AI-assisted automatic proof, it is now in the spotlight.
[12:43] Lean has the distinctive feature of being both a general-purpose programming language and a theorem proof assistant, though it itself is unrelated to AI.
[12:53] The reason it is often discussed alongside AI is that there are opportunities for AI-assisted automatic formalization when translating the natural language and mathematical notation that humans use into computer language — that is, during formalization.
[13:07] In fields with long research histories and well-established theoretical frameworks, enormous research results and methodologies have accumulated. As a result, automatic formalization is expected in some areas.
[13:23] Looking overseas, efforts to advance modern mathematical problems through Lean formalization are being led by Fields Medal laureate Terence Tao, among others.
[13:35] I myself recently attended part of a conference on "AI and Mathematics" at the Institute for Mathematical Sciences at the National University of Singapore,
[13:44] where I encountered interesting team research results on Lean formalization in representation theory and number theory, including the Kazhdan-Lusztig conjecture and affine Deligne-Lusztig varieties.
[13:56] I believe this will become a major trend in mathematical research.
[13:59] Presumably in Japan as well, research using Lean is being attempted in various places.
[14:07] However, organized large-scale efforts are not yet visible. Given this situation, we decided to advance the LANA Project.
[14:15] This project has two objectives.
[14:19] The first is to formalize the main theorems of anabelian geometry — a field where Japanese researchers have made outstanding contributions — in Lean, and to build a library.
[14:29] The second is verification through Lean formalization of Professor Mochizuki Shinichi's Inter-universal Teichmüller theory at RIMS, Kyoto University.
[14:38] This theory has yet to gain broad conviction from the world's mathematicians.
[14:45] Therefore, its verification itself should be deeply meaningful for the advancement of mathematics.
[14:51] With Professor Katō at the center, we have assembled an international team unparalleled in the world for achieving these objectives.
[14:59] Although it is a limited thematic area, I believe this is the best conceivable team in the world.
[15:06] This is a new challenge for our university.
[15:08] Thank you for your attention today.
[15:11] Thank you, President Wakayama.
[15:16] Next, ZMC Director Katō Fumiharu will explain the project.
[15:25] Professor Katō, please go ahead.
[15:27] I am Katō Fumiharu.
[15:30] Thank you very much for gathering here today.
[15:34] At today's press conference, we formally announce that we have launched a new endeavor called the LANA Project.
[15:45] Regarding this LANA Project —
[15:49] until today, we have not disclosed anything about it, including its very existence.
[15:56] However, including its preparatory period, this project has actually been underway since around autumn 2023.
[16:05] The project began in earnest in September 2024,
[16:12] so it has in fact been operating for over a year and a half already.
[16:20] We call it LANA, taking the acronym [Lean + ANabelian].
[16:31] Let me discuss the objectives of this project.
[16:36] There are broadly two objectives.
[16:42] The first objective is the formalization of anabelian geometry and the construction of its library.
[16:48] Anabelian geometry is an important field of arithmetic geometry where Japanese researchers have been particularly prominent.
[16:59] In the LANA Project, we aim to formalize the main theorems and their proofs of this anabelian geometry
[17:06] using the proof assistant Lean on computers,
[17:12] and to build that library.
[17:15] At the same time,
[17:16] we aim to promote the spread of Lean and community formation within Japan's mathematics community.
[17:23] To that end, we plan to organize various events such as research workshops.
[17:29] That is the first objective.
[17:33] The second objective is
[17:35] to verify Professor [Mochizuki's] Inter-universal Teichmüller theory,
[17:41] commonly known as IUT theory,
[17:44] likewise through Lean formalization.
[17:49] Without favoring any particular position,
[17:53] from a neutral standpoint,
[17:55] we aim to organize the theory into a formalizable form,
[17:59] carry out its verification,
[18:01] and thereby put an end
[18:04] to the years-long controversy surrounding this theory.
[18:09] To achieve these goals,
[18:12] this project has
[18:13] assembled a powerful team from around the world.
[18:17] I am proud to say that this team is
[18:21] truly the best in the world
[18:23] for achieving these objectives.
[18:26] Now let me introduce the LANA members —
[18:30] the core members of the LANA Project.
[18:34] There are five core members.
[18:37] From Utrecht University:
[18:40] Johan Commelin.
[18:42] From the University of California, San Diego:
[18:45] Kiran Kedlaya.
[18:46] From the Research Institute for Mathematical Sciences, Kyoto University:
[18:50] Hoshi Yuichiro.
[18:51] From the University of Alberta: Adam Topaz.
[18:55] And myself, as project leader:
[18:58] Katō Fumiharu.
[18:59] In addition to these core members,
[19:03] about seven junior members including students and postdocs
[19:06] are also participating.
[19:08] Commelin, Kedlaya, and Topaz are joining this press conference online,
[19:16] and will give speeches later.
[19:18] Hoshi Yuichiro is absent due to other commitments,
[19:22] but I have received a message from him
[19:24] which I will read on his behalf later.
[19:26] There is one point I'd like to mention about these members' track record.
[19:35] In December 2020,
[19:37] Fields Medal laureate Peter Scholze —
[19:40] who is also famous for publicly expressing
[19:44] a negative view of IUT theory —
[19:47] issued a challenge that launched
[19:50] the Liquid Tensor Experiment,
[19:53] a formalization project in modern mathematics.
[19:57] This was completed in Lean in July 2022,
[20:01] just a year and a half after Scholze's challenge.
[20:07] This event served as an occasion to demonstrate to the world
[20:12] the power of Lean formalization.
[20:16] In fact, it was none other than our project members
[20:21] Johan Commelin and
[20:25] Adam Topaz who led
[20:27] the team that completed the Liquid Tensor Experiment.
[20:29] I was in fact deeply struck by this event,
[20:33] and it led me to conceive
[20:35] of this LANA project.
[20:37] Here I would like to briefly explain
[20:42] formalization of mathematics using Lean.
[20:45] Lean is
[20:47] a functional programming language that is one of
[20:50] the so-called proof assistants.
[20:53] When you hear the term "proof assistant,"
[20:56] you might imagine something that
[21:00] proves mathematical theorems
[21:02] in place of humans,
[21:06] but that is definitely not the case.
[21:08] Ordinary mathematical arguments are
[21:11] typically written using natural language such as Japanese or English
[21:14] combined with mathematical notation.
[21:18] In contrast, formalization using proof assistants like Lean —
[21:23] "formalization" —
[21:25] corresponds to
[21:26] rewriting such mathematical arguments
[21:28] into a programming language.
[21:33] In other words,
[21:34] it amounts to translation from natural language
[21:35] to formal language.
[21:39] To do this,
[21:41] one must eliminate as much ambiguity as possible from natural language
[21:46] and fill in the gaps between the lines that have been omitted.
[21:49] Therefore,
[21:51] formalization can be described as the work of organizing
[21:52] the logical structure of mathematical arguments
[21:55] into a more rigorous
[21:56] and more shareable form.
[22:02] However,
[22:02] IUT theory is
[22:04] a massive and complex theory,
[22:06] and regarding its soundness,
[22:08] the opinions of the world's mathematicians are still divided.
[22:11] Therefore, its formalization
[22:14] cannot be a mere mechanical translation —
[22:16] even assuming such a thing were possible.
[22:23] We ourselves, who carry out the work,
[22:26] must have sufficiently deep [understanding of IUT theory].
[22:32] For this reason, in the LANA Project,
[22:35] over more than a year,
[22:37] we have engaged in intensive discussions about IUT theory.
[22:42] We held boot camps in various locations —
[22:46] Japan, Canada, the Netherlands, the United States —
[22:48] read papers and various other materials,
[22:52] organized the issues,
[22:54] and built the foundation for verification
[22:56] while cross-checking our mutual understanding.
[23:00] As a result,
[23:07] I am proud to say we have come to share a deep understanding among the members. Through this, we can now clearly articulate how far we truly understand and where and how things remain unresolved. And importantly, we have become able to express those still-unresolved points in plain mathematical language.
[23:37] What I must state carefully here is this: at present, we have not yet reached a final conclusion as to whether that point represents a mathematical gap or stems from limitations of our own understanding. Mathematics is an objective discipline, and to put it in a way that is faithful to that objectivity:
[24:07] purely as a possibility, we do think the possibility of a deficiency in the argument at this point certainly exists. Therefore, this is precisely the critical point going forward, and we intend to continue examining it from a strictly neutral standpoint and to continue our dialogue with Mochizuki.
[24:31] Let me speak about the outlook going forward. We plan to present an interim report on the LANA Project's activities to the world in the form of a press conference on July 17 of this year.
[24:46] At that venue, we intend to organize and publish the details of our understanding of IUT theory verification up to that point.
[24:55] This will include not only what we have understood, but also what we have not yet understood, and how we have articulated and positioned those points.
[25:07] In other words, by the July 17 press conference, we intend to compile these issues and our verification results at that point as an interim report and present them to the world.
[25:21] We believe that by pursuing deep mathematical understanding and rigorous computer-based verification in parallel, we can open new horizons in mathematical research.
[25:35] The LANA Project is a challenge toward that goal.
[25:39] We intend to continue facing this task with sincerity and perseverance.
[25:47] Now, let me hand over to our online participants for their speeches.
[25:54] First, Johan Commelin will speak about the significance of Lean formalization in future mathematical research and the need for community building in Japan.
[26:06] Adam Topaz will comment on how Lean may fundamentally change the way mathematical research is done, and on the current status and outlook of our research on IUT theory.
[26:20] Kiran Kedlaya will discuss his own involvement with IUT theory and the impact that computer-based formalization of mathematics will have on the future of mathematics.
[26:32] That concludes my presentation.
[26:35] Thank you for listening.
[26:38] Thank you, Professor Katō.
[26:41] We will now introduce our online speakers.
[26:45] First, Johan Commelin.
[26:49] Johan Commelin is an assistant professor at Utrecht University and director of the Mathlib Initiative.
[26:58] He specializes in number theory, geometry, and category theory, and promotes the formalization of mathematics using the theorem proof assistant Lean.
[27:07] He is one of the leaders of the Liquid Tensor Experiment,
[27:11] and as a maintainer of the mathematical library Mathlib,
[27:15] he contributes to the construction of research infrastructure.
[27:17] Professor Commelin, please go ahead.
[27:22] I would like to thank you for the opportunity to add a few words of my own.
[27:37] As Professor Katō mentioned, Adam Topaz and I led the Liquid Tensor Experiment. After that project was successfully completed, people would ask us about verifying IUT theory.
[28:07] People asked us about this.
[28:27] My answer was that I would be willing, provided that Japanese researchers with IUT expertise were involved.
[28:39] You can imagine my excitement when Professor Katō subsequently contacted me to propose launching the LANA Project.
[28:52] First of all, I am very happy to be collaborating with ZMC on building a formalization and Lean community within Japan's mathematics community.
[EN] [29:12] I believe that mathematics is a conversation between informal intuition and formal rigor.
[EN] [29:18] Lean and mechanization of mathematics play an increasing role in this dialogue.
[29:23] [interpreter] I believe that mathematics is a dialogue between informal intuition and formal rigor. In this dialogue, Lean and the mechanization of mathematics will play an increasingly important role going forward.
[EN] [29:41] I am proud to collaborate with ZMC on spearheading this effort during our boot camps and conferences.
[29:47] [interpreter] I am very proud to collaborate with ZMC in leading this effort through boot camps and conferences.
[29:58] As part of the LANA Project, we are building the foundations of anabelian geometry in Lean — for example, the theory of Galois groups and fundamental groups.
[EN] [30:21] We are now seeing foundational parts of algebraic, arithmetic, and anabelian geometry contributed to the Mathlib library.
[EN] [30:28] It is a solid foundation to build other projects of formal mathematics on top of.
[30:32] [interpreter] Currently, foundational parts of algebraic geometry, arithmetic geometry, and anabelian geometry are being contributed to the Mathlib library. This is becoming a solid foundation upon which to build other formal mathematics projects.
[30:49] Finally, by using Lean, we can make claims and arguments in IUT absolutely precise and rigorous.
[31:34] Generative AI synthesizes text based on statistical patterns, so it can hallucinate — that is, generate incorrect information.
[31:44] In contrast, Lean verifies mathematical truth based on strict logical rules.
[31:49] This eliminates the ambiguity that often arises in informal presentations of mathematics.
[32:12] Furthermore, proofs verified in Lean provide guarantees of correctness that are unachievable through traditional peer review processes.
[32:59] Next, Adam Topaz. Adam Topaz is an associate professor at the University of Alberta and senior manager of the Mathlib Initiative. His specialties are formalization of mathematics, algebra, number theory, and algebraic geometry. He is a leading figure in the formalization of mathematics using Lean, and he led the Liquid Tensor Experiment, a major formalization project in mathematics.
[33:30] Professor Topaz, please go ahead.
[33:37] OK, thank you.
[33:41] I hold a somewhat unusual position among mathematicians.
[34:00] I work across both aspects of this project.
[34:04] I specialize in anabelian geometry, but at the same time I am deeply involved in formal verification using Lean.
[34:13] From my experience working seriously in both of these fields, I have come to realize firsthand how formalization changes the way one thinks about mathematics. This is precisely what the LANA Project is about.
[34:48] Mathematics has been done the same way for thousands of years. We write arguments in natural language,
[35:04] [interpreter] Mathematics has been conducted the same way for thousands of years. We write arguments in natural language,
[35:13] share them with colleagues, and make judgments about whether they are correct.
[35:18] But formalization pushes us to take mathematics one step further.
[35:40] Formalization teaches us not only to be completely explicit and precise,
[35:46] but also to reconsider and optimize the mathematical concepts we use.
[35:54] The formalization process still requires human effort and creativity.
[36:02] [interpreter] The process of formalization nevertheless still requires human power and creativity.
[36:09] What the proof assistant does is check internal logical consistency.
[36:28] That [whether the mathematics is correct and meaningful] remains a question that only human mathematicians can answer.
[36:55] Traditional verification processes can break down. Even well-meaning mathematicians, reading carefully and honestly, can arrive at completely different conclusions.
[37:33] It is with precisely that spirit that we have been working on IUT.
[37:35] As Professor Katō mentioned, over approximately the past year and a half,
[37:49] our team has devoted great effort to building a deep, shared understanding of IUT, always with formalization in mind.
[38:07] There is a specific point in IUT theory that we have repeatedly encountered throughout this project. We have tried multiple approaches, deepening our understanding of IUT theory each time.
[38:37] We have now reached the stage where we can express this point with enough precision to formalize it in Lean — but we have not yet been able to go further beyond that.
[39:08] Whether this situation reflects a true gap in the proof or a limitation of our own current understanding of IUT — we cannot state definitively at this point.
[EN] [39:29] Let me also reiterate what Professor Kato said earlier. We intend to continue the examination of this point and our dialogue with Professor Mochizuki. We believe that the precision provided by Lean will make this dialogue more productive and transparent than has previously been possible.
[39:49] [interpreter] I would like to reiterate what Professor Katō said. We intend to continue our examination of this point and our dialogue with Mochizuki. We believe that the precision afforded by Lean will make this dialogue more productive and transparent than has previously been possible.
[40:19] The mathematical community needs clear answers about this unclear issue, and we are committed to pursuing them with integrity and rigor.
[40:43] Finally, I am deeply grateful to Mr. Kawakami, Professor Katō, and ZMC for assembling and supporting this team with such serious purpose. I am proud to be a member of this project, and I look forward to sharing our progress with the world.
[EN] [41:11] Thank you very much!
[41:16] Thank you, Professor Topaz.
[41:20] Next, Kiran Kedlaya.
[41:24] Kiran Kedlaya is a professor at the University of California, San Diego.
[41:30] He specializes in number theory and arithmetic algebraic geometry,
[41:35] and is known as an authority on p-adic Hodge theory and p-adic differential equations.
[41:42] He has received numerous awards including AMS Fellow and Guggenheim Fellow.
[41:48] Professor Kedlaya, please go ahead.
[41:54] I am a newcomer to the field of mathematical formalization, but my interest in IUT theory goes back long before the LANA Project began.
[42:17] In 2015, a workshop was held at Oxford University, where many arithmetic geometers who had not previously encountered IUT
[42:38] read Mochizuki's papers, gave presentations, and worked together to try to understand the topic.
[42:54] This 2015 workshop, while it did not produce a breakthrough in the community's confidence in IUT, was very enlightening.
[43:45] I myself had stepped back from active research on IUT during that period, but I stayed in occasional contact with some experts and attended additional conferences on the topic. And at those conferences, I was able to confirm that what had appeared to be contradictions were in fact
[44:16] due to miscommunication.
[44:19] Therefore, at present, I consider the status of IUT to still be unresolved.
[44:35] I joined the LANA Project both to stay abreast of the formalization revolution and to help support consensus-building on the current status of IUT and the ABC conjecture.
[45:01] Should this project reach a positive conclusion about IUT, I personally intend to use my social capital to disseminate this conclusion among mainstream researchers in arithmetic geometry.
[45:28] One of the things I learned early on is Adam's point that formalization goes far beyond mere software.
[45:45] It is also a sociological issue — in order to construct correct mathematics using new tools, we must also consider how mathematicians reach consensus on correctness.
[46:25] As proofs of influential theorems become increasingly complex, their verification comes to depend on a fragile network of trust among mathematicians. While AI shows great potential for managing complexity, the unreliability of large language models risks undermining that fragile trust.
[46:55] The LANA Project points the way forward — maintaining focus on promoting human understanding while aided by sophisticated software tools.
[47:15] I very much look forward to the ongoing work of this project team, and I thank Professor Katō and ZMC for making this research possible.
[47:35] Thank you.
[47:42] Thank you, Professor Kedlaya.
[47:44] Finally, Hoshi Yuichiro.
[47:47] Hoshi Yuichiro is an associate professor at RIMS (Research Institute for Mathematical Sciences), Kyoto University.
[47:55] He specializes in arithmetic geometry, particularly arithmetic geometry related to hyperbolic algebraic curves,
[48:03] researching from the perspectives of anabelian geometry and inter-universal Teichmüller theory.
[48:10] Unfortunately, Professor Hoshi is unable to attend today, but he has sent a message, which Director Katō will read on his behalf.
[48:27] As one of the core members of the LANA Project, I have been participating in this project since 2024 and working together with the members.
[48:46] My role was to explain the contents of IUT theory as comprehensively as possible to the LANA Project members.
[49:06] On particularly important points, I took as much time as possible to explain carefully, striving to share not just a rough understanding but the logical details.
[49:19] In particular, building a shared understanding among the members of the logic leading from Theorem 3.11 to Corollary 3.12 in the third paper of IUT theory, published in 2021 —
[49:32] that was one of the major goals I have been working toward.
[49:41] To that end, I spent a long time in discussion, repeated explanations, and organized the issues from as many angles as possible.
[49:49] As a result, through this more than one year of effort, I am convinced that the members' understanding of IUT theory has definitely advanced significantly.
[50:01] At least among those outside IUT theory's direct circle, I do not think there are many people who have attempted to understand it this seriously and worked at it this persistently.
[50:14] That is what I believe.
[50:16] In that sense, I feel this project has great significance, and I am very glad to be participating in such a project.
[50:28] However, at the same time, I unfortunately feel that I have not yet fully fulfilled my role.
[50:36] In particular, regarding the logic leading from Theorem 3.11 to Corollary 3.12 that I mentioned earlier —
[50:45] the fact that many members of the LANA Project feel there is some insurmountable wall within it —
[50:53] I must take that fact seriously.
[50:57] And I strongly feel my own inadequacy in the face of this situation.
[51:04] Even so, I do not think at all that the more than one year of accumulated work has been meaningless.
[51:10] Rather, precisely because we have thought so seriously, discussed, and tried to understand, where the true difficulty lies has become far clearer than before.
[51:23] In that sense as well, I believe the work accumulated in this project has definite value and significance.
[51:32] Finally, I would like to express my deep gratitude to the ZEN Mathematics Center and Professor Katō Fumiharu.
[51:40] Without their extensive support and dedication, this meaningful activity would never have been possible.
[51:47] That is an indisputable fact.
[51:50] Thank you truly.
[51:52] I will continue to face the remaining challenges sincerely and to make every effort to advance the members' understanding even a little further.
[52:01] Thank you.
[52:07] We will now take questions from members of the press present in the venue.
[52:15] Please raise your hand if you have a question.
[52:19] I will call on you; please state your affiliation and name first, then you may remain seated while speaking.
[52:30] Also, for questions directed to the online speakers, there will be consecutive interpretation, so please keep your sentences short, pausing after each one.
[52:41] Does anyone have a question?
[52:54] Q: Professor Katō — IUT theory is inherently difficult to understand, and you've spent a year and a half in discussion and meetings deepening your understanding. How do you intend to verify that the work of translating it into language that Lean can process is correct?
[53:17] Katō: Thank you for the question. That is indeed a very difficult point. It sits at the boundary between the computer and human understanding. That is precisely where the difficulty of this work lies. First, we humans must properly understand the theory — where its importance lies, what characterizes it, what constitutes correctness — and only then translate it into formalized language. Of course, if the program runs without errors, that's good, but beyond that, we believe additional verification is necessary. Therefore, even in the interim report, we recognize that simply showing Lean code and saying "done" is not sufficient. We intend to prepare supplementary manuscripts in ordinary language — in the form of ordinary papers — so that people can read them and be convinced.
[54:42] Q: Are you considering using AI in that translation work?
[54:48] Katō: Not at the present time. For the most critical point — deriving 3.12 from 3.11 — I fundamentally want this to be done by human hands. For other points — foundational parts, to avoid making them black boxes — partially using AI in the process of building those up is a possibility.
[55:20] Q: You mentioned wanting to continue dialogue with Professor Mochizuki. What kind of cooperative framework currently exists, what communication have you had so far, and how do you plan to cooperate going forward?
[55:37] Katō: Our project has been operated with the goal of maintaining near-complete independence from Mochizuki. That remains the current structure. Of course, we don't ignore him — if Professor Mochizuki provides various information, we will of course consider it as reference, and we have done so on some points. That said, we maintain our position as purely questioners vis-à-vis Mochizuki. In the process of asking questions and receiving answers, communication naturally occurs.
[56:42] Q: Professor Katō — you've mentioned several times that there's a point where it's unclear whether it's a mathematical gap or a limitation of understanding. Is that specifically referring to the logic from 3.11 to 3.12? What exactly is the problem, and why can't you proceed with formalization?
[57:16] Katō: Thank you for the question. To put it bluntly, it is in the middle of deriving 3.12 from 3.11.
[57:26] Q: So conversely, if that point is cleared, would you say the path to formalization is essentially open?
[57:33] Katō: That's a difficult question, but I expect that is roughly the case.
[57:46] Q: In the process of formalization, if you found that making such-and-such a modification would allow Lean's consistency check to pass, could proposing corrections to Mochizuki's existing papers be among the project's possible conclusions?
[58:05] Katō: Including that, I think various possibilities exist.
[58:18] Q: Related to the previous question — is communication with Professor Mochizuki currently happening?
[58:34] Katō: Shall I take this? Of course. We are in communication — if we weren't, we couldn't ask questions. Yes, we are.
[58:46] Q: Could you tell us what Professor Mochizuki has been saying?
[58:53] Katō: We haven't specifically asked him what he thinks of this project, so I don't know his true feelings. A clue, however, is that last October 26, Professor Mochizuki released a report to the world on the current status of IUT theory. In it there are about three sections, and in the last section, quite suddenly, he wrote an extremely favorable passage about Lean formalization. Reading that, it seems clear that Mochizuki's view of Lean formalization is not negative at all. By inference, I think he acknowledges a certain level of significance in what we are doing.
[60:12] Q: Related to the previous questions — you're continuing with formalization and there may be a point you can't understand, possibly a mathematical gap. Have you communicated this to Mochizuki?
[60:36] Katō: Yes, we have communicated it.
[60:42] Q: Has there been any reaction? Presumably Mochizuki understands that point — could you share any response?
[60:53] Katō: Well... the reaction... hmm... how should I put it... Basically, our communication is through written text, so what we can read from that is what we have to go on.
[62:31] Katō: I have a personal connection with Shinichi [Mochizuki] — we've spent years doing private seminars together, so there is certainly that foundation. But the point currently at issue in IUT theory is quite technical, and on that point, I had not discussed such things in those seminars, and looking back, my understanding was still insufficient. Now, compared to then, I've made enormous efforts studying over the past year and a half, so my understanding has advanced considerably. But it's still not complete. Precisely because it's not complete, the wall we cannot overcome — whether it's actually a mathematical gap or not — I want to emphasize that both possibilities are equally open. We have not yet reached a definitive conclusion on this. I want to stress that point.
[63:49] Q: You've said there's a problem at the point of deriving 3.12 from 3.11. Can I confirm — for all other points, do you consider the outlook for formalization to be clear for the time being?
[64:11] Katō: Thank you for the question. You said there's a "problem" at 3.11 to 3.12, but I think the more accurate way to put it is that there's a point we don't understand. As for the other points — we haven't fully replicated everything yet, but our shared understanding is that they are probably fine. Of course, formalizing those parts will require various additional processes, but we expect it can be completed in finite time.
[65:00] Q: Apologies for my ignorance, but regarding the derivation from 3.11 to 3.12 — how does this relate to the contradictions pointed out by Professor Scholze and others?
[65:15] Katō: Thank you. On that point, I would prefer to refrain from commenting today. We have a press conference scheduled for July 17, and we intend to discuss it properly there.
[65:38] Q: The July report will be an interim report. What is your outlook for the timeline and scope of work after that?
[65:54] Katō: July is strictly an interim report, and I don't think we'll be able to present a completely final conclusion there. This is a very large, long-term project. I estimate it will take at least several years. We will continue the formalization of important parts and related work.
[67:31] Katō: [continuing from a question about how he first encountered Lean] ...I was asked to be a co-organizer, and that was the beginning. Until then, I knew virtually nothing about Lean — or rather, about proof assistants in general. Then I attended three of Johan's lectures and thought, "Ah, so this is what this world is about."
[68:00] About a year later, the Liquid Tensor Experiment was actually completed. Until then, using computers to assist mathematical research had existed for decades. But the fact that mathematical verification could be done through computer programming — and moreover, that it could be applied to extremely technically difficult problems in modern mathematics — seeing that proof before my eyes, I was truly struck by how the times had changed.
[68:49] Q (to Commelin): Just as Professor Katō was struck by it, the Liquid Tensor Experiment involved very complex, difficult modern mathematics. Compared to that, how do you view the difficulty of the LANA Project — both IUT theory and building the anabelian geometry library — as someone who has been through it?
[71:29] Commelin (interpreter): There are two aspects to this. First, in terms of understanding the mathematical theory — the Liquid Tensor Experiment involved a theory that was well-understood, but as you say, it was very complex modern mathematics, so it was difficult in that respect. But IUT theory also has difficulty in various ways — the gap that was discussed, and the question of whether our human understanding is sufficient.
[EN] [72:09] No worries. Thanks for interrupting me. And then on the other hand, there is the question of formalizing things in Lean. And I would say with the liquid tensor experiment, we've really been pushing Lean
[EN] [72:25] to the edges of its capabilities. We learned a lot from that project. And so in terms of the challenges with formalization, I would say
[EN] [72:40] so far the challenges in the liquid tensor experiment were at least as hard as what we were seeing in the LANA project. So yeah, maybe I should pause again for the translation.
[72:53] [interpreter] Regarding Lean formalization — in the Liquid Tensor Experiment, we also struggled greatly. Through those various struggles and efforts, we were able to learn a great deal. Of course, challenges in formalization exist in the LANA Project as well, and I believe the difficulty is comparable to that of the Liquid Tensor Experiment.
[74:04] Q: I've heard that writing proofs in Lean takes several times or even tens of times more time and effort compared to writing proofs in natural language. Is that still the case, or has the situation changed with the expansion of libraries and the Lean community?
[75:44] Commelin (interpreter): I cannot give you specific numbers, but it is certainly true that even today, using Lean requires more time and effort than expressing things in natural language. A key factor in formalization is creating the necessary prerequisite materials, or finding how to adopt and apply existing materials.
[77:47] Q (to Kedlaya): Regarding the editorial process at PRIMS that published Mochizuki's IUT papers — do you think it was appropriate? Given that first-rate mathematicians are now making great efforts and finding points they can't understand — normally, in a journal paper, peer review would require those points to be made understandable. Yet the papers were published with such points remaining. Do you think the editorial process, including peer review, was appropriate?
[79:15] Kedlaya (interpreter): On that point — when the IUT theory papers were published, it was extremely difficult for the editors to assemble people who could conduct peer review, given how enormously broad the scope of IUT theory was. The situation at the time was that the number of researchers well-versed in IUT theory was very small. That is believed to be the cause.
[80:39] [interpreter continues] Through the peer review process, the goal is to demonstrate whether a mathematical theory is correct and accurate. However, even so, peer review is still a process carried out by humans.
[81:10] Q: So you think the process at the time was not very appropriate?
[81:52] Kedlaya (interpreter): My understanding is that, based on the expertise available within the mathematics community at the time, they made their best efforts and conducted the best peer review possible given the circumstances.
[82:10] MC: Thank you for all your questions. Due to time constraints, we will end the Q&A here.
[82:16] Thank you very much for attending the ZEN Mathematics Center LANA Project announcement today despite your busy schedules.
[82:23] Thank you also to everyone watching online.
[82:27] This concludes the announcement.
[82:31] A photo session will follow here at the venue.
[82:37] We are making preparations, so members of the press, please remain seated for the moment.
[83:05] Thank you.
Transcribed from audio using mlx-whisper (whisper-large-v3-turbo model). Timestamps are approximate. Some artifacts remain, particularly during bilingual sections (English with consecutive Japanese translation) and during silent/transitional passages.
- Wakayama Masato (若山正人) — ZEN University President (~11:00-15:10)
- Katō Fumiharu (加藤文元) — ZMC Director, Project Leader (~15:25-26:35, Q&A)
- MC/Moderator — introductions, Q&A facilitation
- Johan Commelin — online (~27:20-32:20)
- Adam Topaz — online (~33:35-41:15)
- Kiran Kedlaya — online (~41:50-47:35)
- Hoshi Yuichiro (星雄一郎) — message read by Katō (~48:20-52:05)
- Press — Q&A (~52:05-82:10)
[10:49 - 11:17] 本学全数学センターのラナプロジェクト発表の場にお越しいただき感謝申し上げます AI時代に入った現在純粋数学においても本質的な場面でのコンピュータ照明の有効性や可能性の広がりが現実味を帯びています 今日はこのZMCのプロジェクトについてご報告申し上げたく存じます [11:17 - 11:33] プロジェクト名は証明支援系リーンと数論気化学の一分野であるエンアーベル気化学に基づくものですが詳細につきましては後ほどZMC所長であり本プロジェクトの推進を担う加藤文明教授が行います [11:33 - 11:47] 私からはなぜ本日の発表となったかについてご説明申し上げたく思います 本学は本格的なオンライン大学を作ることで日本の深刻な教育格差の [11:47 - 12:01] 緩和解消を図るために昨年4月に開学しました インターネットやAIなどの最新のIT技術を駆使することにより既存の大学では実現が難しかった新しい [12:01 - 12:14] 教育の形を作り上げることを目指しております 一方で大学である限り教育を根底から支え人類の知的財産を豊かにする学問研究もまた大きな柱です [12:14 - 12:26] 前大学では既存の大学ではあまり取り組んでいなかったいくつかのテーマに関する研究を組織的に進めており その一つが今日ご紹介するZMCによるラナプロジェクトです [12:26 - 12:36] 数学においては以前はリーンを使った研究は盛んではありませんでした しかしコンピューターの計算能力の飛躍的向上と [12:37 - 12:43] AIによる自動証明の可能性が伺えるようになり 今や脚光を浴びているものです [12:43 - 12:53] リーンは汎用プログラミング言語でありながら定理証明支援系でもあるという特徴を持ちますが それ自体はAIに無関係です [12:53 - 13:06] AIと共に語られることがあるのは 人間が使う自然言語と数式をコンピューター言語に翻訳する つまり形式化の際にAIによる自動形式化の機会があるからです [13:07 - 13:23] 歴史的に長く研究され 理論体系が整った分野には膨大な研究成果 あるいは方法論が蓄積しております そのため一部ではこの自動形式化も期待されているという次第です [13:23 - 13:35] 海外に目を向けますと 現代数学の問題をリーン形式化によって発展させようという試みが 例えばフィーズ症受賞者であるテレンス・タオラが中心となって進んでいます [13:35 - 13:44] また最近私自身もシンガポール国立大学の数理科学研究所での AIと数学というテーマの会議の一部に出席しまして [13:44 - 13:56] カズアンルスティック予想やアファインドリーン・リースティックバラエティといった 表現論・整数論分野におけるリーン形式化による興味深いチーム研究の成果に 触れてまいりました [13:56 - 13:59] 数学研究の大きな潮流になると考えています [13:59 - 14:07] おそらく我が国においてもリーンを用いた研究が 各所で試みられているとは思います [14:07 - 14:15] しかし組織だって本格的にという姿は見えておりません こうした状況もありラナプロジェクトの推進を決めました [14:15 - 14:19] 本プロジェクトの目的は2つです [14:19 - 14:29] 一つは日本の研究者の貢献が著しい エン・アーベル・キカ学の主要定理をリーン形式化し そのライブラリを構築することです [14:29 - 14:38] もう一つは京都大学数理解析研究所の 餅月慎一教授による宇宙祭対比ミラリ論の リーン形式化による検証です [14:38 - 14:45] この理論については未だ世界の数学者からの 納得感が得られていないままの状況です [14:45 - 14:51] したがってその検証自体が数学の発展にとって 意義深いはずです [14:51 - 14:59] 今回加藤教授が中心となり目的達成のために 世界に比類ない国際チームを整えることができました [14:59 - 15:06] 限られたテーマ分野ではありますが 考え得る世界最高のチームだと思っております [15:06 - 15:08] これは本学の新しい挑戦です [15:08 - 15:11] 本日はどうぞよろしくお願いいたします [15:11 - 15:16] 和歌山学長ありがとうございました [15:16 - 15:25] 続きましてZMC所長の加藤文春より 今回のプロジェクトについてご説明をいたします [15:25 - 15:27] 加藤先生よろしくお願いいたします [15:27 - 15:30] 加藤文春でございます [15:30 - 15:33] 本日はお集まりいただきまして誠にありがとうございました [15:34 - 15:42] 本日の記者発表では私たちが新たにラナプロジェクトというものを開始しましたことを [15:42 - 15:45] 皆様に正式にご報告申し上げます [15:45 - 15:49] このラナプロジェクトについてなんですが [15:49 - 15:56] これは今日まで実は存在も含めて 一切公表して公開してきませんでした [15:56 - 16:01] しかし実はこのプロジェクトは その準備期間も入れますと [16:01 - 16:05] 既に2023年秋ごろから始まっております [16:05 - 16:12] プロジェクトが本格的に始動したのが 2024年の9月ですので [16:12 - 16:14] 実は本格的に始まってから [16:14 - 16:19] もはや1年半以上にわたって 活動を続けているということになります [16:20 - 16:31] アクロニムをとってラナと呼んでいるんですが [16:31 - 16:36] このプロジェクトの目的についてお話しいたします [16:36 - 16:41] このプロジェクトの目的は 大きく分けて2つございます [16:41 - 16:42] アクロニムをとってお話しします [16:42 - 16:48] 第一の目的は エンアーベル気化学の形式化と そのライブラリー構築です [16:48 - 16:54] エンアーベル気化学というのは 従来より日本人の研究者が [16:54 - 16:59] 顕著に活躍している 数論気化学の重要分野になります [16:59 - 17:04] ラナプロジェクトでは このエンアーベル気化学の [17:04 - 17:06] 主要定理とその証明を [17:06 - 17:12] 計算機上の証明支援計リーンを用いて形式化し [17:12 - 17:15] そのライブラリーの構築を目指します [17:15 - 17:16] それと同時に [17:16 - 17:23] 日本の数学界におけるリーンの普及と コミュニティの形成を促す [17:23 - 17:26] そのため研究集会など [17:26 - 17:28] 様々なイベントをですね [17:28 - 17:29] 企画してまいりたいと [17:29 - 17:33] それが第一の目的になっています [17:33 - 17:35] それから第二の目的なんですが [17:35 - 17:41] 教授の宇宙最大ヒムラー理論 [17:41 - 17:44] いわゆるIUT理論を [17:44 - 17:49] 同じくリーンの形式化によって 検証することにあります [17:49 - 17:53] 私たちは特定の立場に偏ることなく [17:53 - 17:55] 中立的な視点から [17:55 - 17:59] 理論を形式化可能な形に整え [17:59 - 18:01] その検証を行うことで [18:01 - 18:04] 同理論に関する長年にわたる論争に [18:04 - 18:09] 終止符を打つということを目指しております [18:09 - 18:12] これらの目標を達成するため [18:12 - 18:13] 本プロジェクトでは [18:13 - 18:16] 世界中から強力なメンバーを集めました [18:17 - 18:21] 私としてはこのメンバーは [18:21 - 18:23] これらの目標を達成する上で [18:23 - 18:25] まさに世界一のメンバーであると [18:25 - 18:26] 自負しております [18:26 - 18:30] それでは次にラナメンバー [18:30 - 18:32] ラナプロジェクトのコアメンバーになりますが [18:32 - 18:34] こちらのご紹介をいたします [18:34 - 18:37] コアメンバーは5名おります [18:37 - 18:40] イヨットレヒト大学の [18:40 - 18:42] ヨハン・コメリン [18:42 - 18:45] カリフォルニア大学サンディエゴ校の [18:45 - 18:46] キラン・ケドラヤ [18:46 - 18:50] 京都大学数理解析研究所の [18:50 - 18:51] 星雄一郎 [18:51 - 18:55] アルバータ大学のアダム・トパーズ [18:55 - 18:58] そして私プロジェクトリーダーの [18:58 - 18:59] 加藤文春です [18:59 - 19:03] これらのコアメンバーのほかに [19:03 - 19:05] 学生やポストドックなどの [19:06 - 19:08] 若手メンバーが7名ほど参加しております [19:08 - 19:12] 今回コメリン・ケドラヤ・トパーズの3子は [19:12 - 19:16] オンラインでこの発表会に参加しておりますので [19:16 - 19:18] 後ほどスピーチをいたします [19:18 - 19:22] 星雄一郎は所要のため欠席しておりますが [19:22 - 19:24] メッセージを預かっておりますので [19:24 - 19:26] 後ほど私が代読いたします [19:26 - 19:29] このメンバーの実績について [19:29 - 19:32] 一つお話ししておきたい点がございます [19:33 - 19:35] 日本の発表会に参加しております [19:35 - 19:37] 2020年の12月にのことなんですが [19:37 - 19:40] フィールド賞受賞者であるピーター・ショルツェ氏 [19:40 - 19:44] この人はIUT理論に対して [19:44 - 19:47] 否定的な見解を公にしていることでも有名なんですけれども [19:47 - 19:50] このショルツェ氏のチャレンジから始まった [19:50 - 19:53] リクイッド・テンサー・エクスペリメントという [19:53 - 19:56] 現代数学の形式化プロジェクトがありました [19:57 - 20:01] これが2022年の7月 [20:01 - 20:04] ショルツェ氏の挑戦からわずか1年半で [20:04 - 20:07] リーンによって完成しました [20:07 - 20:12] この出来事はリーンによる形式化の威力を [20:12 - 20:15] 世界中に示すきっかけともなりました [20:16 - 20:20] 実はこのリクイッド・テンサー・エクスペリメントを [20:20 - 20:21] 完成させたのは [20:21 - 20:23] 他でもない当プロジェクトの [20:23 - 20:25] ヨハン・コメリンと [20:25 - 20:27] アダム・トパーズがリーダーとして [20:27 - 20:29] 主導したチームです [20:29 - 20:33] 実は私はこの出来事に強い衝撃を受けて [20:33 - 20:35] このラナーというプロジェクトを [20:35 - 20:37] 構想するに至ったような次第です [20:37 - 20:42] ここでリーンによる数学の形式化について [20:42 - 20:45] 簡単にご説明したいと思います [20:45 - 20:47] リーンとは [20:47 - 20:50] いわゆる証明支援系と呼ばれている [20:50 - 20:53] 関数型プログラミング言語の一つです [20:53 - 20:56] 証明支援系という言葉を聞くと [20:56 - 21:00] あたかもそれ自体が人間に代わって [21:00 - 21:02] 数学の定理を証明してくれるような [21:02 - 21:06] そういうものを想像するかもしれませんが [21:06 - 21:08] 実はそういうものでは決してありません [21:08 - 21:11] 普通の数学の議論は [21:11 - 21:14] 日本語や英語などの自然言語と [21:14 - 21:17] 数式を併用しながら記述されるのが [21:17 - 21:18] 常なんですけれども [21:18 - 21:22] これに対してリーンなどの証明支援系による [21:22 - 21:23] 形式化 [21:23 - 21:25] フォーマリゼーションですね [21:25 - 21:26] 形式化とは [21:26 - 21:28] そのような数学の議論を [21:28 - 21:32] プログラミング言語に書き換えることに対応しています [21:33 - 21:34] 言い換えれば [21:34 - 21:35] 自然言語から [21:35 - 21:39] 形式言語への翻訳に当たります [21:39 - 21:41] それを行うには [21:41 - 21:46] 自然言語が持つ曖昧さをできるだけ排除し [21:46 - 21:49] 省略されている行間を埋めていかなければなりません [21:49 - 21:51] したがって [21:51 - 21:52] 形式化とは [21:52 - 21:55] 数学の議論の筋道を [21:55 - 21:56] より厳密で [21:56 - 21:59] より共有しやすい形に整える作業であるといえます [22:02 - 22:02] しかしながら [22:02 - 22:04] IUT理論は [22:04 - 22:06] 巨大で複雑な理論であり [22:06 - 22:08] その整備については [22:08 - 22:11] 現在でも世界の数学者たちの意見が分かれています [22:11 - 22:14] したがってその形式化の作業は [22:14 - 22:16] 単なる機械的な翻訳 [22:16 - 22:20] そのようなものが可能だとしての話なんですけれども [22:20 - 22:23] そういう機械的な翻訳では済まされません [22:23 - 22:26] 作業を進める私たち自身が [22:26 - 22:29] IUT理論について十分深い [22:32 - 22:35] そのためラナプロジェクトでは [22:35 - 22:37] 1年以上にわたって [22:37 - 22:42] IUT理論について集中的に議論を重ねてまいりました [22:42 - 22:46] 日本、カナダ、オランダ、アメリカなど [22:46 - 22:48] 各地で合宿を行い [22:48 - 22:52] 論文など各種の資料を読み [22:52 - 22:54] 論点を整理し [22:54 - 22:56] 互いの理解を突き合わせながら [22:56 - 22:59] 検証のための土台を築いてまいりました [23:00 - 23:01] その結果として [23:07 - 23:37] 理解をメンバーの中で共有できているようになったと自負しております。それによって私たちはどこまでちゃんと理解できていて、どこがどのように解明できていないのか、明瞭に言い表されるようになってきました。そして重要なのは、その未だ解明できていないポイントを平易な数学の言葉で表現できるようになったということです。 [23:37 - 23:37] ここで慎重に申し上げるべきは、現時点でそのポイントが数学的なギャップであるのか、それとも私たち自身の理解力の問題に由来するのかについて、私たちはまだ最終的な結論を出していないということです。数学とは客観的な学問ですが、その客観性に忠実な言い方をするとして、 [24:07 - 24:31] あくまでも可能性としてなんですが、この点に議論の不備があるという可能性はもちろんあると思っています。ですから、まさにこの点こそが今後の革新的論点であり、私たちは今後もこの点について、あくまでも中立な立場から検討を進め、餅月氏との対話も続けていくつもりです。 [24:31 - 24:45] 今後の見通しについて申し上げます。私たちは、今年の7月17日に、ラナプロジェクトの活動に関する中間報告を記者会見の形で世界に向けて発表する予定です。 [24:46 - 24:55] その場では、IUT理論の検証について、その時点までの我々の理解の詳細を整理して公表したいと考えています。 [24:55 - 25:06] そこには私たちが理解できた点だけでなく、まだ理解できていない点、そしてそれをどのように言語化し、どのように位置づけているかということも含まれます。 [25:07 - 25:21] そしてそれを言い換えれば、私たちは7月17日の記者会見までに、これらの論点とその時点での検証結果を中間報告としてまとめ、世界に提示するつもりです。 [25:21 - 25:34] 私たちは、数学の深い理解と計算機による厳密な確認等を並行して追求することによって、新しい数学研究の地平を切り開くことができると信じております。 [25:35 - 25:38] ラナプロジェクトは、そのための挑戦です。 [25:39 - 25:45] 引き続き、誠実に、粘り強く、この課題に向き合ってまいりたいと思っております。 [25:47 - 25:53] それでは、引き続きまして、この後はオンライン参加者たちにスピーチしてもらうことになります。 [25:54 - 26:05] まず、ヨハン・コメリンが、将来の数学研究におけるリーン形式化の意義や、日本におけるコミュニティ形成の必要性などについてお話しいたします。 [26:06 - 26:19] アダム・トパーズからは、数学研究のやり方がリーンによって大きく変わる可能性があること、そしてIUT理論をめぐる我々の研究の現状と展望についてコメントしてもらいます。 [26:20 - 26:31] キラン・ケドライアからは、彼自身のIUT理論との関わりや、コンピューターによる数学の形式化が将来の数学にもたらすインパクトについて話してもらいます。 [26:32 - 26:35] それでは、ここで私の話は終わりとさせていただきます。 [26:35 - 26:36] ご静聴ありがとうございました。 [26:38 - 26:40] 加藤先生、ありがとうございました。 [26:41 - 26:44] では、ここからオンライン登壇者をご紹介いたします。 [26:45 - 26:48] まずはじめに、ヨハン・コメリン氏です。 [26:49 - 26:57] ヨハン・コメリン氏は、ユトレヒト大学の助教で、マスリブイニシアティブのディレクターを務めておられます。 [26:58 - 27:06] 数論、幾何学や語り論を専門とし、定理証明支援系リーンによる数学の形式化を推進。 [27:07 - 27:10] リキッドテンサーエクスペリメントのリーダーの一人でもあり、 [27:11 - 27:13] 数理ライブラリーマスリブのメンテナーとして、 [27:15 - 27:17] 研究インフラ構築に貢献していらっしゃいます。 [27:17 - 27:20] それでは、ヨハン・コメリン氏様、お願いいたします。 [27:20 - 27:22] プロフェッサー・コメリン、おばあさん。 [27:22 - 27:37] 我就に述べたように、私からも一言、我就に加えさせていただく機会をいただき、感謝を申し上げたいと思います。 [27:37 - 28:07] 先ほど加藤教授がおっしゃったように、アダム・トパーズと私は、リクイッド・テンソル・エクスペリメントを指導してまいりました。そのプロジェクトが成功理に終了した後のち、人々からIUT理論の検証に、 [28:07 - 28:13] 人々から問われることがありました。 [28:13 - 28:21] 私の答えは、日本のコミュニティ、人々のIUT理論の人たちに、人々のアイスプレーティーが入っています。 [28:21 - 28:27] 私の感想を想像して、私の感想を想像していることを、プロフェッサー・カートを発表したいと思います。 [28:27 - 28:35] 私の答えは、IUTの専門知識を持つ日本の研究者たちが関与していただけるのであれば、 [28:36 - 28:39] その鍵において、創出するというものでした。 [28:39 - 28:52] そして、その後、加藤教授から、ランナープロジェクトの立ち上げを提案するご連絡をいただいたときの、私の興奮ぶりは、ご想像いただけるかと思います。 [28:52 - 29:05] まずは、日本の数学コミュニティ内に、形式化、 [29:05 - 29:12] およびリーンコミュニティを構築するにあたり、ZMCと協力できることをとても嬉しく思います。 [29:12 - 29:18] I believe that mathematics is a conversation between informal intuition and formal rigor. [29:18 - 29:22] Lean and mechanization of mathematics play an increasing role in this dialogue. [29:23 - 29:32] 私の信念は、数学というものは、非形式的な直感と、それから、形式的な厳密さとの対話であると信じております。 [29:32 - 29:39] この対話において、リーンや数学の機械化は、ますますこれから大切な役割を果たしていくと考えています。 [29:41 - 29:47] I am proud to collaborate with ZMC on spearheading this effort during our boot camps and conferences. [29:47 - 29:57] ブートキャンプや、カンフェランスを通じて、この取り組みをリードしていくために、ZMCと協力できることをとても誇りに思います。 [29:58 - 30:15] 次に、LANAプロジェクトの一環として、リーンを用いた円アーベル機化学の基礎を構築しています。 [30:15 - 30:20] 例えば、ガロアテンや基本群の理論などであります。 [30:21 - 30:26] We are now seeing foundational parts of algebraic, arithmetic and anabelian geometry contributed [30:26 - 30:28] to the Mathlib library. [30:28 - 30:32] It is a solid foundation to build other projects of formal mathematics on top of. [30:32 - 30:43] 現在、大数気化学、数論気化学、そして円アーベル気化学の基礎的な部分が Mathlib library に寄稿されつつあります。 [30:43 - 30:49] これは他ほかの形式数学プロジェクトを構築するための強固な基盤となっていきます。 [30:49 - 31:19] 最後にこのリンを使用することでIoT における主張や論章を絶対的に正確かつ厳密なものにすることができます [31:34 - 31:43] 生成AIは統計的パターンに基づいてテキストを合成していくためハルウシネーションすなわち誤った情報を生成する可能性があります [31:44 - 31:49] 対照的にリンは厳格な論理規則に基づいて数学的な真意を検証していきます [31:49 - 32:11] これにより数学の非公式な提示におけるしばしば生じる曖昧さが排除されるということになります [32:12 - 32:19] またリンで検証された証明は従来のピアレビュープロセスでは達成不可能な正しさの保証を提供します [32:59 - 33:29] 続きましてアダム・トパーズ氏です。アダム・トパーズ氏はアルバータ大学の準教授でマスリブイニシアティブのシニアマネージャーを務めておられます。専門は数学の形式化、大数学、数論、大数幾何学。リーンを用いた数学の形式化における指導者的存在であり、数学の巨大な形式化プロジェクトリキッドテンサーエクスペリメントを主導されました。 [33:30 - 33:33] それではアダム・トパーズ様、お願いいたします。 [33:34 - 33:36] それではプロフェッサー・トパーズ、パッシングオーバーとしております。 [33:37 - 33:38] OK、ありがとうございました。 [33:41 - 33:59] 私は数学者の中ではやや珍しい立場にあります。 [34:00 - 34:04] このプロジェクトの両方の点にわたって研究を行っています。 [34:04 - 34:13] 私はエン・アーベル機化学を専門としておりますが、同時にリーンを用いた形式検証にも深く関わっています。 [34:13 - 34:43] この両方の分野で本格的に取り組んできた経験からも この形式化が数学に対する考え方をいかに変えていくかということを身をもって実感してまいりました これこそがまさにこのランナープロジェクトが [34:48 - 34:53] マテマティックスは千歳のようにしています 自分の言語を書いています [34:53 - 34:57] 自分の言語を書いています 友達と共同の言語を共有しています [34:57 - 35:04] 自分の言語を合わせることができるかもしれません でもフォーマリゼーションは少し進めます [35:04 - 35:12] 数学というものは数千年にわたり同じ方法で進められてまいりました 我々は自然言語で論章を書き [35:13 - 35:18] それを同僚と共有して それが正しいかどうかについて判断を下していきます [35:18 - 35:25] しかし形式化というものが我々をこの数学をさらなる一歩を求めていくことになります [35:27 - 35:33] フォーマリゼーションは全て説明していまして でもまた全て説明していまして [35:33 - 35:38] またまた全て説明していまして マテマティマティコンセプトを使ってみます [35:40 - 35:46] 形式化というものは我々が完全に明示的かつ正確であることを 教えるということだけではなくて [35:46 - 35:52] さらに我々が用いる数学的概念を再考し 最適化するということも教えることになります [35:54 - 36:02] フォーマリゼーションプロセスは 人間の努力と創造性が求められていきます [36:02 - 36:07] 形式化のプロセスにはそれでも依然として 人間の動力と創造性が求められていきます [36:09 - 36:22] 証明支援系が行うのは内部的な論理的一貫性を チェックすることであります [36:28 - 36:30] これが依然として人間の数学者だけが答えられる問題です [36:55 - 37:25] 経緯的な検証プロセスは機能しなくなることがあります。 良識ある数学者であっても、また注意深く誠実に読み解いたとしても、全く異なる結論に達してしまうことがあるのです。 [37:33 - 37:35] まさにその精神を持って、私どもはIoTに取り組んでまいりました。 [37:35 - 37:49] カト教授がおっしゃったように、私どもはおよそ過去1年半の理由を提供しています。 [37:49 - 38:07] 私たちのチームは常に形式化を念頭に置きながら、IoTに対する深く共有された理解を築いていくために大きな努力を注いでまいりました。 [38:07 - 38:37] IUT理論にはこのプロジェクトを通じて繰り返し遭遇した特定の点がございます。私どもはこの多角的なアプローチを試み、その度にIUT理論に対する理解をどんどん深めてまいりました。 [38:37 - 39:00] 現在この点をですね、リーンで形式化できるほどの精度で明確に表現できる段階に達しておりますが、しかしこれからさらにその先へ進むことが現状ではまだできておりません。 [39:08 - 39:27] IUT理論にはこのような状態がこの証明における真のギャップを反映しているのか、それとも私たち自身の現在のIUT理解の限界なのか、現時点では断定的に述べることはできません。 [39:29 - 39:49] Let me also reiterate what Professor Kato said earlier. We intend to continue the examination of this point and our dialogue with Professor Muchizuki. We believe that the precision provided by Lean will make this dialogue more productive and transparent than has previously been possible. [39:49 - 40:11] 加藤教授がおっしゃったことを改めて強調したいと思います。私どもはこの点についての検討をさらに進めて継続し、そしてまた餅月との対話を継続するつもりでおります。リーンがもたらす精密さによってこれまでの対話よりもより生産的で透明性の高いものになると信じております。 [40:19 - 40:32] 数学会においてはこの不明瞭な問題について明確な説明が必要となっており、私どもは誠実かつ厳密にその追求に取り組んでまいります。 [40:36 - 40:43] 最後に言ってください。私はこのプロジェクトに委員会を提供していると嬉しいです。 [40:43 - 41:09] 最後になりますが、川上氏、加藤教授、ZMCがこのような真剣な目的意識を持ってこのチームを結成し支援してくださっていることに深く感謝を申し上げます。私はこのプロジェクトの一員であることを誇りに思っておりまして、そして私どもの進捗状況を世界と共有できることを楽しみにしております。 [41:11 - 41:12] Thank you very much! [41:12 - 41:13] ありがとうございます! [41:13 - 41:15] どうもありがとうございました! [41:16 - 41:18] トパズ様、ありがとうございました。 [41:18 - 41:20] Thank you, Professor Topaz! [41:20 - 41:24] 続きまして、キラン・ケドラヤ氏です。 [41:24 - 41:30] キラン・ケドラヤ氏はカルフォルニア大学サンディエゴ校の教授を務めておられます。 [41:30 - 41:35] 数論及び数論大数幾何学を専門とし、 [41:35 - 41:42] P-Cin-Hodge理論や、P-Cin-微分方程式などの権威として知られます。 [41:42 - 41:48] AMSフェローや、グッケンハイム・ヘッフェローなど多数の賞を受賞されています。 [41:48 - 41:52] それでは、キラン・ケドラヤ様、お願いいたします。 [41:54 - 42:15] 私は数学生形式化の分野では信頼者ではありますが、IUT理論への関心は、ラナープロジェクトが始まるずっと前から持っておりました。 [42:17 - 42:37] 2015年、オクスフォード大学でワークショップが開催され、それまでIUTに触れたことのなかった多くの数論幾何学者が、 [42:38 - 42:47] 餅津市の過去の論文を読んだり、また発表したりするなどして、一丸となってこのテーマを理解しようと努めました。 [42:48 - 42:52] このワークショップは、IUT理論に関することができません。 [42:54 - 43:04] この2015年のワークショップは、IUTに対する学会の理解において、画期的な信頼をもたらすほどではありませんでしたが、非常に啓発的なものでした。 [43:45 - 44:15] 私自身もこの当時その時期はIUTに関する研究を控えておりましたがしかし一部の専門家とは時折連絡を取り合っていましたそしてこのテーマに関する追加の会議にも集積していましたそしてその会議で矛盾のように見えたものは実は [44:16 - 44:19] コミュニケーションの行き違いによるものであったということを確認できました [44:19 - 44:34] したがって現在において私はIUTに関してその現状は依然として未解決であるというふうに考えております [44:35 - 45:00] 私はこの軽視化革命の動向を把握するとともにIUTおよびABCオスオの現状に関するそういった合意形成を支援していくためにもこのLANAプロジェクトに参加いたしました [45:01 - 45:27] このプロジェクトがIUTについて肯定的な結論に達した暁には私自身は社会的資本を通じてこの結論がですね数論的科学の主流の研究者たちに広めるつもりがあります [45:28 - 45:44] 私が初期段階で学んだことの一つはですね形式化が単なるソフトウェアの枠を遥かに超えているというアダム先生のご指摘です [45:45 - 46:08] これは社会学的な問題でもありますつまり新しいツールを用いて正しい数学を構築するためには数学者が正しさについてどのように合意に至るのかについても考慮していかなければなりません [46:25 - 46:53] 影響力のある定理の証明がますます複雑化するにつれてその検証は数学者間の脆弱な信頼のネットワークに依存するようになってまいりました しかしAIは複雑さを制御する上で大きな可能性を示しているもののそういった中で大規模言語モデルの信頼性の低さというものがその脆弱な信頼を損なうリスクをもたらすものです [46:55 - 47:14] ランナープロジェクトはこういった洗練されたソフトウェアツールの助けを借りつつ人間の理解を促進するために焦点を当て続ける今後の道筋を示していくものでございます [47:15 - 47:35] 今後将来にわたってこのプロジェクトチームの継続的な取り組みを非常に楽しみにしておりますとともにこの研究を可能にしてくださった加藤教授およびZMCに感謝を申し上げます [47:35 - 47:36] ありがとうございました [47:36 - 47:38] どうもありがとうございました [47:39 - 47:41] ありがとうございました [47:42 - 47:44] Thank you, Professor Kennaia [47:44 - 47:47] 最後に、星雄一郎氏です [47:47 - 47:55] 星雄一郎氏は京都大学数理解析研究所リムスの準教授を務めておられます [47:55 - 48:01] 数論幾何学、特に双極的台数曲線に関わる数論幾何学を専門とし [48:03 - 48:10] エナーベル幾何学やPC対ヒュミラー理論の観点から研究を進める数学者です [48:10 - 48:19] 星様は残念ながら本日ご欠席となりますが、メッセージを頂戴しておりますので、加藤所長より代読させていただきます [48:19 - 48:20] 加藤先生お願いいたします [48:20 - 48:24] はい、それでは星雄一郎メンバーですが、あのメッセージを私、加藤が代読いたします [48:27 - 48:41] 私はラナプロジェクトのコアメンバーの一人として、2024年からこのプロジェクトに参加して、メンバーの皆さんと一緒に活動してまいりました [48:46 - 49:04] 私はラナプロジェクトのメンバーに対して、IUT理論の中身をできるだけ網羅的に説明することでした [49:06 - 49:17] 特に重要なポイントについては、できるだけ丁寧に時間をかけて説明し、単なる概略理解にとどまらず、論理の細部まで共有できるよう努めてまいりました [49:19 - 49:25] 特に2021年に出版されたIUT理論の第三論文に書かれている [49:25 - 49:32] 定理3.11から計3.12を導く論理に対する共通理解 [49:32 - 49:39] それをメンバーの中でしっかりと構築することを一つの大きな目標として、これまで取り組んでまいりました [49:41 - 49:49] そのために長い時間をかけて議論を重ね、説明を繰り返し、できるだけ多くの角度から論点を整理してきました [49:49 - 50:00] その結果として、この1年以上の努力を通じて、メンバーのIUT理論に対する理解は確実に大きく前進したと確信しています [50:01 - 50:14] 少なくともIUT理論の直接の関係者以外で、これほど真剣にその理解を試みて、そしてこれほど粘り強く取り組んだ人たちはそれほど多くない [50:14 - 50:16] 私はそのように思います [50:16 - 50:26] その意味で、このプロジェクトには大きな意義があると感じていますし、またそのようなプロジェクトに参加していることを、私はとても嬉しく思います [50:28 - 50:36] しかし同時に、残念ながら、私はまだ自分の役割を完全には果たせていないと考えています [50:36 - 50:43] 特に、先に述べた定理3.11から計3.12を導く論理について [50:45 - 50:53] 7プロジェクトのメンバーの多くが、その中に何か超えられない壁があると感じていること [50:53 - 50:57] その事実を、私は重く受け止めなければなりません [50:57 - 51:03] そして、そのような状況に対して、自分自身の至らなさも強く感じています [51:04 - 51:10] それでも、私はこの1年以上の積み重ねが無意味であったとは全く思いません [51:10 - 51:22] むしろ、ここまで真剣に考え、議論し、理解しようとしてきたからこそ、どこにその本当の難しさがあるのかが、以前よりもはるかに明確になったのだと思います [51:23 - 51:32] そのような意味においても、このプロジェクトで積み重ねてきた営みは、確かな価値と意義があると考えています [51:32 - 51:40] 最後に、全数学センター及び加藤文春教授に対して、深く感謝を申し上げます [51:40 - 51:47] これまでの様々な多大な支援と尽力なくしては、この有意義な活動は決してありえなかった [51:47 - 51:50] そのことは疑いようのない事実です [51:50 - 51:52] 本当にありがとうございます [51:52 - 52:01] 今後も残された課題に対して、誠実に向き合いながら、メンバーの理解を少しでも前に進める努力を続けていきたいと思います [52:01 - 52:03] ありがとうございました [52:03 - 52:05] 以上です [52:05 - 52:07] 加藤先生、ありがとうございました [52:07 - 52:15] それではここで、会場にお越しの記者の皆様から、ご質問をお受けしたいと思います [52:15 - 52:18] ご質問のある方は、挙手をお願いいたします [52:19 - 52:29] そしてまた私から指名をさせていただきますので、まずはご所属とお名前をおっしゃっていただいて、その後おかけになったままお話いただければと思います [52:30 - 52:41] またですね、オンライン登壇者への質問の場合は、逐次通訳が入りますので、できるだけ文を短く、一文一文で止めていただきながらお話いただけますと幸いです [52:41 - 52:44] それでは、どなたかご質問はございますでしょうか [52:44 - 52:48] はい、じゃあ真ん中の女性の方、お願いいたします [52:49 - 52:51] はい、どうぞ [52:52 - 52:54] 共同通信の田島と申します。よろしくお願いいたします [52:54 - 53:08] 加藤先生の質問なんですけれども、そもそもIUT理論というのは、理解するのが難しくて、先生方も1年半かけて議論をして、ミーティングを積み重ねて、理解を深めてきたというところですけれども [53:08 - 53:17] これをリーンが読み取れるような言語に翻訳する作業が正しいかどうかという検証は、どのように行っていくおつもりでしょうか [53:17 - 53:22] はい、ご質問ありがとうございます。そこは非常に難しいところだと思います [53:22 - 53:31] いわゆるその、コンピューター、計算機と、それから人間の理解の境目のところっていう、そういう位置づけになるかと思います [53:32 - 53:40] やはりそこが、この作業の非常に難しいところかなというふうに思います [53:40 - 53:50] まずは我々人間が、きちんと理解して、理論を理解して、どこに重要性があるのかとか [53:50 - 53:57] それから、どういうところがこの理論の特徴なのかとか、何をもって正しいとするのかとか [53:57 - 54:04] そういったことも十分検討した上で、形式化された言葉に翻訳していくという作業がなければいけないと [54:04 - 54:09] もちろんそれで、エラーなくプログラムが通ればそれでいいんですけど [54:09 - 54:14] それだけじゃなくて、最後にまた検証が必要であるというふうに考えています [54:14 - 54:19] したがって、中間発表でもそういうことになると思うんですが [54:19 - 54:25] 単にリーンコードを皆さんにお見せして、はい、できました、で済まされる話ではないというふうに認識しています [54:25 - 54:31] それに対して我々は補足する形で普通の言語で書かれたというか [54:31 - 54:35] 普通の論文の形のマニスクリプトもちゃんと用意していきたいと [54:35 - 54:40] つまりそれを読まれて、皆さんが納得するという形のものも用意していきたいというふうに考えております [54:40 - 54:42] ありがとうございます [54:42 - 54:46] その翻訳作業で、例えばAIを使ったりということはお考えなんでしょうか [54:48 - 54:52] 今のところ考えてはいないんですけれども [54:52 - 54:58] その一番重要なポイントですね、3.11から3.12を導く部分に関しては [54:58 - 55:03] 基本的には鉄道鉄道人間の手でやっていきたいなと私は考えています [55:04 - 55:10] それ以外のポイント、言ってみれば基礎的な部分のそこをブラックボックスにしないために [55:10 - 55:14] その部分の積み上げをつくっていくというプロセスにおいては [55:14 - 55:18] 部分的にAIを併用するということはあり得るかもしれません [55:19 - 55:20] ありがとうございます [55:20 - 55:25] 餅月先生とも対話を詰め重ねていきたいということをおっしゃっていたんですが [55:25 - 55:29] 今現在どのような協力体制をまず強いているのかということと [55:29 - 55:31] これまでどのようなコミュニケーションを取られて [55:31 - 55:36] 今後どのように協力していくのかというところも教えてください [55:37 - 55:42] 餅月さんとは、我々のプロジェクトというのは [55:43 - 55:48] ほぼ完全な独立性を保つということを目標としてやってきてまして [55:48 - 55:51] 現在でもそういう体制でやっております [55:51 - 55:55] もちろん餅月さんを無視するというわけではないわけで [55:55 - 55:59] 餅月先生から寄せられる様々な情報があった場合には [55:59 - 56:03] もちろんそれを参考にするということは可能性としてはございますし [56:03 - 56:06] そういうことを今までやってきたということも [56:06 - 56:08] いくつかの点に関してはございます [56:10 - 56:11] そういうわけですから [56:11 - 56:16] 我々は餅月さんに対して [56:16 - 56:20] あくまでも質問者であるという立場で貫いていくわけですが [56:20 - 56:25] その質問してその答えを得るという過程においては [56:25 - 56:29] 当然コミュニケーションが生じるというふうに理解していただいて結構です [56:30 - 56:31] ありがとうございました [56:31 - 56:33] はい [56:33 - 56:36] ではその他にご質問ある方 [56:36 - 56:38] 一番後ろの加賀さん [56:38 - 56:42] マイクをお願いします [56:42 - 56:49] NHKの記者の加賀ですよろしくお願いします [56:49 - 56:51] 加藤先生にお伺いしたいんですけれども [56:52 - 56:55] 何度か数学的な問題があって [56:55 - 56:57] 数学的なギャップなのか [56:57 - 57:02] 理解力の問題に由来するのかというところがまだはっきりしないというようなお話が何度かありましたけれども [57:02 - 57:09] それは具体的に3.11から3.12の論理のところのことを指しているのか [57:09 - 57:11] どういった点が問題になっていて [57:11 - 57:15] その形式化というところで先に進めないという状況になっているのかというのを改めて教えていただければ [57:16 - 57:18] はい質問ありがとうございます [57:18 - 57:24] ズバリ言って3.11から3.12を出す途中の場所にそれがあります [57:24 - 57:26] ありがとうございます [57:26 - 57:33] じゃあ逆に言えばそこさえクリアすればもう形式化への道は開けたも同然というように考えていらっしゃるんでしょうか [57:33 - 57:36] 難しい質問だと思うんですけれども [57:36 - 57:41] ほぼそういうことになるんじゃないかなと私は期待しております [57:41 - 57:44] ありがとうございます [57:46 - 57:51] あとあの例えばこの形式化の過程であの例えばこういうふうに修正をすれば [57:51 - 57:55] このリーンにおける一貫性の証明チェックができるというふうになった場合に [57:55 - 58:02] 例えば既存の持続議論文に対して何かこう修正点を示して提案するみたいなことも [58:02 - 58:05] このプロジェクトの結論としてはあり得るんでしょうか [58:05 - 58:09] まあそれも含めてあの様々な可能性はあり得ると思います [58:09 - 58:11] わかりましたありがとうございます [58:13 - 58:14] ありがとうございます [58:14 - 58:18] それでは一番前の男性お願いいたします [58:18 - 58:25] 日本経済新聞の矢野と申しますよろしくお願いします [58:26 - 58:29] 先ほどの方の質問に関連するんですが [58:29 - 58:34] 現時点で餅月先生とのコミュニケーションというのは取れているんでしょうか [58:34 - 58:35] それは私でよろしいですか [58:35 - 58:36] はい [58:37 - 58:38] もちろんです [58:38 - 58:40] 取れていますっていうか [58:40 - 58:42] 取れてなかったら質問できないので [58:42 - 58:43] はい [58:43 - 58:44] 取れてます [58:46 - 58:48] 餅月先生はどういうふうにおっしゃってるかっていうのを [58:48 - 58:50] もし教えていただければ [58:52 - 58:53] はい [58:53 - 58:59] 具体的にこのプロジェクトをどう思いますかというような話はしたことがないので [58:59 - 59:04] どう思ってるかっていうのはそれは本心のところはわからないわけですけど [59:06 - 59:15] 手がかりになるのはやはりその昨年10月26日に餅月新一教授が世界に向けてですね [59:15 - 59:21] IUT理論の現状に関するリポートをリリースされております [59:23 - 59:26] その中で3つほどセクションがあるんですけど [59:26 - 59:28] その中の最後のセクションで [59:29 - 59:30] 突如としてですね [59:30 - 59:36] リーン形式化に対する極めてその好意的な記事を書かれているんですね [59:37 - 59:39] それを読む限りにおいては [59:39 - 59:44] リーンを用いた形式化に対する [59:46 - 59:47] もちづき氏のその見解というのは [59:47 - 59:50] 決して悪くはないということは [59:50 - 59:51] まあ明白だと思います [59:52 - 59:53] そこからの類推して考えるに [59:54 - 59:56] 我々がやっていることに対しても [59:56 - 60:01] まあある一定の意義は認めていらっしゃるんじゃないかなというふうに思います [60:02 - 60:03] ありがとうございます [60:05 - 60:10] それでは一番前の男性にお願いいたします [60:12 - 60:15] 朝日新聞の石倉といいます [60:15 - 60:18] 今の関係に関連の質問なんですけれども [60:19 - 60:22] 今景色化を続けていて [60:23 - 60:25] 理解できないポイントがあるかもしれない [60:25 - 60:27] 数学的なギャップかもしれないということなんですけど [60:28 - 60:31] それは餅月さんにはもう伝えていらっしゃるんでしょうか [60:32 - 60:33] 私よろしいですね [60:34 - 60:35] ありがとうございます [60:36 - 60:39] はい伝えてます [60:42 - 60:44] 何か反応というかですね [60:44 - 60:46] 餅月さんはその理解できないポイントは [60:47 - 60:48] もちろん理解してるんだと思うんですけども [60:49 - 60:52] 何か反応とかをお示しいただけることがあればお願いします [60:53 - 60:54] そうですね [60:55 - 60:56] あのその [60:58 - 60:59] まあ何 [61:00 - 61:01] あの [61:01 - 61:02] 反応ですか [61:03 - 61:04] あの [61:05 - 61:07] どう言ったらいいのかな [61:07 - 61:08] その [61:08 - 61:09] まず [61:10 - 61:14] 基本的にあのコミュニケーションが文章を通じてしてますので [61:14 - 61:15] ある意味その [61:16 - 61:17] そこから読み取れること [61:18 - 61:19] っていう [61:20 - 61:21] ことがまあ [61:21 - 61:22] キーになってくる [61:22 - 61:24] それしかないんだというふうに思います [61:25 - 61:26] まあ [61:27 - 61:28] 何か [61:32 - 61:33] その [62:31 - 63:01] 新一さんとは個人的なつながりがあり 何年もプライベートでセミナーを積み重ねてきたっていう そういった確かにベースはあるんですがかなりIUT理論で実際 今問題になっているポイントっていうのはかなり技術的な側面であり その点に関して私たちは私はそのセミナーではそういうことは議論してこなかったということもあり また私自身はやはり今から振り返ってみるとその点に関してまだまだ理解が足りなかったなというふうに [63:02 - 63:15] 今現在はそれに比べると確かにものすごく努力して この1年半ぐらいは勉強させていただきましたのでかなり理解は進んだというふうに考えています でもまだ完全じゃないと思っています [63:15 - 63:26] 完全じゃないからこそそこにある我々が乗り越えられない壁というものが その実際数学的なギャップなのかそれともそうじゃないのか [63:27 - 63:41] 両方とも同じように可能性があるということは強調しておきたいんですが そのそれに関して私たちは完全にあの結論を出すに至ってないということですね ここをちょっと強調しておきたいと思います [63:41 - 63:42] ありがとうございました [63:42 - 63:49] はいでは続いてその後ろの男性にお願い致します [63:49 - 63:55] 4ミリ新聞の小山と申しますよろしくお願いいたします あの加藤先生にあの質問させていただきたいんですけれども [63:56 - 64:03] 定理3.11から3.12を導く点にちょっとあの今あの問題点があるというふうにおっしゃってましたが [64:03 - 64:11] 確認にありますがその他の点については形式化については今の今を差し当たっては見通しがついているという理解でよろしいでしょうか [64:11 - 64:21] はい質問ありがとうございます 3.11から3.12にあの問題点があるとおっしゃいましたけれどもその我々が分かってない点があるというのが正式な [64:21 - 64:24] あの言い方正式なというか正確な言い方かなというふうに思います [64:24 - 64:35] でそれ以外の点に関するご質問なんですが あのそれ以外の点に関してはあの我々はまだまだあの完全なその追試っていうのはしてないんですけれども [64:35 - 64:39] まああの基本的な我々が持っているその共有 [64:39 - 64:50] その理解としてはおそらく問題ないだろうという認識でありますもちろんそこを形式化するためにはまたその部分をこうあの形式化に [64:50 - 65:00] その理解を避うような形でまた書き直していくとかまあ様々なあのプロセスは必要になってきますけれどもおそらく有限の時間内で終わることなのじゃないかという認識でいます [65:00 - 65:15] すいませんあの不勉強で大変恐縮なんですけどその3.11から3.12への導出に関してはその小津先生の小津先生とかの指摘にされている矛盾点との関係性でいきますとどのようなことになりますでしょうか [65:15 - 65:28] はいありがとうございますその点についてはできればあの今日はちょっとあのコメントは差し控えさせていただきたいと考えています [65:28 - 65:38] あの7月17日のあの記者会見こちらの方予定しておりますがそちらではきちんとお話ししたいと考えています [65:38 - 65:44] ありがとうございますあと最後にですねあのまあ7月の報告はの中間報告という形になります [65:44 - 65:54] あの後についてですねあのどれくらいの期間をかけてどのようなことを行っていくというふうにあの見通しを持っていらっしゃいますでしょうか [65:54 - 65:57] はいえーと [65:57 - 66:27] 7月はあくまでも中間報告でおそらくその場で完全に最終的な結論は出せないと思いますやはりこれは非常に大きな長い時間のかかるプロジェクトだと私は認識しています少なくとも数年はかかるというふうに考えていますので引き続き継続して重要な部分の形式化ないしは形式化に付随する仕事などを [67:27 - 67:30] 我就は我就は我就は我就は我就我就我就我就我就我就我就 [67:31 - 67:42] 頂まれて共同のオーガナイザーになってくれと言われたのが始まりだったんです その時まで僕はリーンというものはリーンどころかいわゆるプルーフアシスタントと呼ばれている [67:42 - 67:54] あのまあ一種の何ですかねその証明支援系ですけどそういったものに対してはほとんど何も知らなかった状況でした それがあのヨハンのレクチャーを3回聞いて [67:54 - 68:00] なるほどこういう世界があるのかということを初めて知ったような次第です [68:00 - 68:10] それから1年ぐらい経って実際にそのリキッドテンサーが完成したんですね その時まさにそのまあ [68:10 - 68:23] それまでもですね計算機を使ってその数学の研究の補助にするとか そういったことってのはまあ何十年も前からあったと思うんですね [68:23 - 68:33] なんですがまさにその数学の検証をそのコンピューターのプログラミングでできるんだっていう [68:33 - 68:39] しかもそれが現代数学の極めて技術的に難しい問題に対してあのアプライできるということ [68:39 - 68:49] その実証が目の前にあるっていうことを見てすごい時代が変わったなっていうか あの小さいう意味で衝撃を受けたってことですね [68:49 - 69:01] あとえっと小銘先生にも伺えればと思うんですけれどもえっとあのそのまあ加藤先生が衝撃を受けられたようにそのリキッドテンサーエクスペリメントってすごくまあえっと [69:02 - 69:13] 複雑で難しい現代数学だったということなんですけれどもそれと比べて今回のそのランナープロジェクトが大衆生IoT理論とかあるいはの [69:13 - 69:21] AIブリック科学のこうあのライブラリを作っていくっていう作業というのはまあ比べてその大変さとか難しさとかなんかあのその辺を比べとどんな [69:21 - 69:26] あのものとまあ経験者としてご覧になっているかということをちょっと伺えたらと思うんです [71:29 - 71:57] この点に関しましては2つの面があると思います まず1点目 まずその数学理論の理解としてはこのリクイルテンソールエクスペレメントの方はですね 数学理論としてはよく理解をしようとしていましたが 仕上げりがおっしゃる通り非常に複雑なそういった現代数学であるということがございまして その点では難しかったですし しかしまたAUT理論においてもいろいろな面で難しさがあり 先ほどの話を出たギャップですとか [71:57 - 72:07] そしてこれをそれが果たして私どもの人間の理解が至っていないことによることなのかどうかということがわからないという現状があります [72:07 - 72:09] Could you please continue? I'm sorry [72:09 - 72:25] No worries. Thanks for interrupting me. And then on the other hand, there is the question of formalizing things in Lean. And I would say with the liquid tensor experiment, we've really been pushing Lean [72:25 - 72:39] to the edges of its capabilities. We learned a lot from that project. And so in terms of the challenges with formalization, I would say [72:40 - 72:52] So far the challenges in the liquid tensor experiment were at least as hard as what we were seeing in the LANA project. So yeah, maybe I should pause again for the translation. [72:53 - 73:01] 一方ですねその Leanの形式化ということに関しまして 形式化において Leanを用いていくということに関してなんですが [73:01 - 73:10] その点においてはこのリクイド・テンソル・エクスペリメントにおきましても非常に苦心いたしました。 そしてそういったいろいろな苦心、努力をしながら [73:10 - 73:22] 非常に多くのことをその過程で学ぶことができました。 もちろんこのLANAプロジェクトにおいてもその形式化ということをしていく上でのチャレンジが存在し、それはこのLean [73:22 - 73:29] リクイド・テンソル・エクスペリメントと同じくらいの難しさ、困難さというものが LANAプロジェクトにもあると考えています。 [73:29 - 73:57] と言うことをまとめて申し上げますと、このチャレンジというものは数学的なチャレンジにおいては、この議員というものの形式化を使って解決していくことが、 [73:58 - 74:02] 理員の形式化を使って解決していくことができるというふうに考えております。 [74:02 - 74:04] 大きゅう。 [74:04 - 74:22] すみません、もう一つコメントに伺いたんですけど、 普通に自然言語で証明を書くのに比べて、景色化で、Leanで証明を書くと数倍とか数十倍とかの時間や手間がかかるということを聞いたことがあるんですけれども、 [74:23 - 74:43] そういう状況というのは以前の話だったのか、今もそのライバラリーとか、あるいはLeanのコミュニティの拡大とかで、そういう状況が変わってきているのか、その辺のちょっと、Leanで景色化していくところの手間とか時間の問題について、ちょっと現状を教えてください。 [75:44 - 76:14] 何枚かという数字を申し上げることは [76:15 - 76:20] 今においても今日においても自然言語で表現するよりも [76:20 - 76:24] リーンを用いていくものはより多くの時間 [76:24 - 76:28] そして努力を必要とするということは確実に言えると思います [77:06 - 77:36] そこにおいて 例えば 事前必要な プレリクイズというようなマテリアルを作成していく あれは既存のマテリアルをいかに採用 適用していくかということが その形式化をしていく上でのことということになります [77:37 - 77:43] 手前から2列目のシャツの男性 お願いいたします [77:47 - 78:01] 共同通信の辻村といいますけど ケドラヤさんに伺いたんですけどIoTの餅月さんの論文を載せたP-RIMSの編集作業ということについて 妥当だったと思いますかっていうのは これだけね [78:02 - 78:26] 第1線の数学者が努力して ここからここは分からないっていうポイントが出てくるっていうのは 普通のジャーナルのペーパーであれば そこはピアレビューで分かるようにしなさいとか なんとかすると思うんですね なのにもかくはらず そういう点が残ってしまったまま パブリッシュされているということについて そのピアレビューを含めた編集作業ということについて 妥当だったと思うかどうかっていうお考えを伺えてないですか [79:15 - 79:43] その点に関してはですね [79:44 - 79:47] このAUT理論の論文が公開されたときには [79:47 - 79:54] 編集者側でなかなかこのAUT理論があまりにも広範囲に [79:54 - 79:55] 縦に渡っているということ [79:55 - 79:59] そしてそういった広範囲に対するそういった形での [79:59 - 80:03] ピアレビューをしていく人たちを揃えるのが非常に難しかったという現状 [80:03 - 80:06] 当時の状況があったというふうに理解をしております [80:06 - 80:11] このAUT理論に関して精通をした研究者というものが [80:12 - 80:14] 非常に少なかったということが原因だと考えられます [80:39 - 81:09] プロセスと言うことによって数学理論が正しいかどうか正確かどうかということを示していくことになるわけですがしかしそうは言ってもピアレビュープロセスと言ってもやはり人間が行うプロセスですから [81:10 - 81:31] その通りのプロセスはあまり適切ではなかったというふうにお考えなんでしょうか [81:52 - 82:04] 数学界自体における専門性に基づいて最善の努力をして、そこの当時でできる最善のピアレビューをしたという認識でおります [82:04 - 82:08] よろしいでしょうか [82:10 - 82:11] では、たくさんご質問いただきましてありがとうございます [82:11 - 82:16] 大変恐縮ではございますが、ご時間の関係上、こちらで最後とさせていただきます [82:16 - 82:23] 本日はお忙しい中、全数学センター新プロジェクトランナーの発表会にご参加いただきまして誠にありがとうございます [82:23 - 82:27] また、オンラインの皆様もご視聴いただきありがとうございました [82:27 - 82:31] これにて発表会は終了とさせていただきます [82:31 - 82:35] この後、会場ではフォトセッションのお時間とさせていただきます [82:37 - 82:40] 準備を行いますので、記者の皆様は今しばらくお席にいてお待ちくださいませ [82:40 - 82:44] フォトセッション [83:05 - 83:06] ありがとうございました
Essay on the module “Conjecture – abc in relation to the number zero”
In the context of Neomodern Science (NS), the module “Conjecture – abc in relation to the number zero” offers a fundamental exploration of the concepts that form the basis for understanding numbers, points, and their interrelations. This module situates the central natural law within an informal logic that encompasses not only abstract but also concrete aspects of reality. This essay examines the propositions and concepts presented in this module, focusing on the implications of bounded and unbounded numbers and their role in geometry.
Unbounded versus bounded
The module states that in NS, the product of an unbounded number of points and an infinitesimally small number of points is not equal to zero. This idea is crucial because it forces us to reflect on the nature of numbers and the dimensions in which they exist. In traditional mathematics, it is often assumed that multiplying any number by zero always yields zero, but according to the principles of NS, there is a nuance to be made. The unboundedness of the points implies that there is a potentially infinite amount of information or dimension present that cannot simply be reduced to a single value of zero.
On the other hand, when we consider a bounded number of points multiplied by an infinitesimally small number of points, the result is indeed zero. This concept can be seen as a reflection of the way finite and infinite numbers interact. It provides a valuable foundation for understanding the geometric structures that surround us and emphasizes the need to consider both abstract and concrete values.
The role of the number one
The number one, referred to as the first natural number, plays a crucial role in this module. In the context of NS, one is not merely a number but a concept that lays the foundation for understanding unity and identity within geometry. The concept of “one” as the first entity allows us to construct other numbers and values, thereby forming the foundation of the numerical hierarchy. This understanding is essential for building complex structures in science and mathematics and is therefore indispensable in the analysis of the central natural law.
Bounded values and their meaning
The module also addresses the idea that the bounded element in proposition 10 (non-number) can have multiple values, referring to a quantity of interconnected line segments. This idea reflects an abstract reality in which different geometric forms and structures can be combined to create new concepts. This versatility is vital for developing a well-founded geometry that enables us to understand and model the complexity of nature.
At the same time, it is stated that the same bounded element in proposition 10 can also have a single value, representing a concrete object such as a Planck particle with one dimension. This dualism between abstraction and concrete representation is a powerful feature of NS, allowing us to explore both theoretical and practical applications. It emphasizes the need to understand the relationship between abstract numbers and concrete objects and provides a framework for studying nature on a deeper level.
Conclusion
The module “Conjecture – abc in relation to the number zero” offers an in-depth exploration of the concepts of boundedness and unboundedness and their implications for Neomodern Science. By highlighting the interaction between abstract and concrete values, this module enables us to better understand the complexity of natural science. It provides not only a theoretical foundation but also practical insights into how we can perceive and apply numbers and their relationships in reality. The integration of informal logic with the central natural law strengthens the reliability and depth of the knowledge acquired within NS.