26/06/13 09:10:34.88 TTzQJf42.net
つづき
追加 ホイヨ
URLﾘﾝｸ(ivanfesenko.org)
News – Ivan Fesenko
・IUT and Lean: S. Mochizuki’s talk at a workshop on AI and math theorem provers on April 10
URLﾘﾝｸ(aitpm.github.io)
Workshop on AI and Theorem Provers in Mathematics
AITPM
Recordings
URLﾘﾝｸ(www.youtube.com)
A video playlist of the workshop is available on YouTube.
URLﾘﾝｸ(youtu.be)
Shinichi Mochizuki: On the Formalization of IUT: a preliminary progress report
exlean
2026/04/15
In this talk, we survey preliminary work conducted by my research group at RIMS, Kyoto University, since the fall of 2025 on the long-term project of formalizing IUT (inter-universal Teichmüller theory). This work began with the organization of this project into various stages (Stages 1～5) and revolves (not so much around writing complete Lean code for the mathematical content of IUT in its entirety, but rather) around the idea that Lean can utilized as a communication tool for recording the precise logical structure of key portions of the logic of IUT in such a way that Lean code can be used to communicate this logic in a more precise and effective way than conventional natural language- based mathematical discourse to mathematicians who have professional expertise in writing Lean code (i.e., who, unlike my research group at RIMS, have the capacity to generate substantial quantities of professionally written Lean code). Finally, we discuss in detail, as a sort of case study, the reorganization into suitable blackboxes, from a Lean formalization-oriented point of view, of the logic of the final portion “3.11⇒3.12” of the third paper on IUT, since it is this portion of IUT that has received the most public attention. The skeletal Lean code that we wrote for this portion of IUT constituted a remarkably successful case of the use of Lean as a communication tool.
つづく