25/10/29 13:59:54.14 nBZNRF1I.net
>>853-854
>なんかあっちのスレでicmをleanに打ち込んで検証してるという人出てるから、応援する気なら正しいと信じてる人みんなで手分けして Lean に打ち込んでみればいいんじゃないか？
おお、ありがとう！
そういえば 下記 Conference Name: ZMC Conference 2025
Dates: July 1 - July 4, 2025
どうなったんだ、加藤？
”We will also work in small groups to actually work on the formalization of mathematics related to anabelian geometry by Lean4. ”
とか
アウトプット出せ！ 加藤！！
そうしないと、信用されなくなるよ・・・
URLﾘﾝｸ(zen.ac.jp)
ZMCカンファレンス2025 開催のお知らせ
2025.02.20
Conference Name: ZMC Conference 2025
Title: Anabelian Geometry and its Computer Formalization
Dates: July 1 - July 4, 2025
Organizers:
Johan Commelin (Utrecht)
Yuichiro Hoshi (RIMS, Kyoto)
Fumiharu Kato (ZMC)
Kiran Kedlaya (UCSD)
Adam Topaz (Alberta)
Conference Theme:
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.