ZMC Conference 2026

ZEN数学センター（ZEN Mathematics Center; 略称 ZMC https://zen.ac.jp/zmc）では、以下の研究集会を企画しております。

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

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

【参加方法】：要予約、無料
【参加予約URL】： こちらのGoogle フォームよりお申し込みください。

※ 注意：Registrationの締切は7月3日です。Registration を行うとすぐに詳しい参加日程と参加形態（対面かオンラインか）を問い合わせる2つ目のフォームのURLが送られてきます。そちらのフォーム（2つ目）は日程等の詳細が決まり次第お送りください（7月6日締め切り）。上のフォーム（1つ目）では、参加日程・形態については現時点で分かる範囲のおおまかな情報だけで結構です。

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

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

数論幾何学や代数幾何学以外のご専門の数学者の方々のご出席も歓迎いたします！

【各セッションの内容】：
・午前：数論幾何学のコンピューター形式化やAIによる自動形式・自動定理証明に関するセッションを行います。

　Speakers:
　　Christian Merten (Utrecht)
　　Dagur Asgeirsson (Alberta）
　　Andrew Yang (Imperial College London）
　　園田翔（RIKEN AIP）
　　笠浦一海（Omron Sinic X）
　　Jiang Jiedong (Peking university)
　　Guoxiong Gao (Peking university)
　　...and more TBA

・午後：計算機による形式化に関するチュートリアルに引き続いて、小グループによる作業（Group work）を行います：参加者がいくつかの小グループに分かれて、実際に体験することでコンピューター形式化に入門し、数論幾何学の命題・補題などの実際の形式化に取り組みます。

皆様のご参加を歓迎致します。