ZMC Conference 2025

• Johan Commelin (Utrecht)
• Yuichiro Hoshi (RIMS, Kyoto)
• Fumiharu Kato (ZMC)
• Kiran Kedlaya (UCSD)
• Adam Topaz (Alberta)

Recently, more and more people have become interested in the formalization of mathematics by computers, and are becoming more and more aware that Lean4 formalizations and verifications of mathematics have the potential to significantly change the way of doing the research mathematics in the future. These formalizations have already been applied to various areas of arithmetic geometry, and at this conference we would like to discuss the potential of Lean4 formalization of anabelian geometry. In this conference, we would like to discuss not only the latest research presentations on anabelian geometry, but also the construction of libraries related to anabelian geometry. We will also work in small groups to actually work on the formalization of mathematics related to anabelian geometry by Lean4. The conference will also include a session on automatic formalization by machine learning.