https://zen.ac.jp/zmc/activities/d5ov5qajb
【タイトル】：Arithmetic geometry, AI, and Lean
【日程】：2026年7月21日（火）～23日（木）
【開催地】：東京都中央区銀座4-12-15 歌舞伎座タワー12F ドワンゴセミナールーム

【オーガナイザー】：
　　Johan Commelin（Utrecht）
　　星裕一郎（京都大学数理解析研究所）
　　加藤文元（ZMC）
　　Kiran Kedlaya（UCSD）
　　Adam Topaz（Alberta）

【テーマ】：
　近年、コンピュータによる数学の形式化に興味を持つ人が増えており、Lean4による数学の形式化と検証が、将来の数学研究のやり方を大きく変える可能性があると認識されつつあります。さらに、最近ではAIによる自動定理証明や、AIを用いた未解決問題の解決など、数学研究への人工知能の進出が多く見受けられるようになりました。今回のZMC研究集会では、数論幾何学や代数幾何学のコンピューター形式化を出発点として、数学者視点から、AIによる自動形式化や自動定理証明について取り上げたいと考えています。

本会議では、昨年と同様に、小グループに分かれて、実際にLean4を用いて数論幾何学に関連する数学の形式化に取り組む、3日間のグループワークも行います。