The ZEN Mathematics Center (ZMC) is organizing the following research conference. 【Title】: Arithmetic geometry, AI, and Lean 【Dates】: Tuesday, July 21, 2026 - Thursday, July 23, 2026 【Venue】: Dwango Seminar Room, 12F Kabukiza Tower, 4-12-15 Ginza, Chuo-ku, Tokyo 【Organizers】: 　　Johan Commelin (Utrecht) 　　Yuichiro Hoshi (Research Institute for Mathematical Sciences, Kyoto University) 　　Fumihito Kato (ZMC) 　　Kiran Kedlaya (UCSD) 　　Adam Topaz (Alberta) 【How to Participate】: Registration required, free of charge 【Registration URL】: <a href="https://docs.google.com/forms/d/1YLTuuU5u3l4QGgR-X0BokQFL6UUUeYEsIxIaxDuyAWg/viewform?edit_requested=true">https://docs.google.com/forms/d/1YLTuuU5u3l4QGgR-X0BokQFL6UUUeYEsIxIaxDuyAWg/viewform?edit_requested=true</a> ※ N.B. Upon completing this Registration, you will immediately receive a URL for the second form to inquire about your detailed participation schedule and attendance type (in-person or online). Please submit that form (2nd form) once your schedule and other details are finalized (deadline: July 6). For this form (above Google form), only general information about your participation schedule and type you currently know is sufficient. 【Theme】: In recent years, interest in computer-based formalization of mathematics has grown, and it is increasingly recognized that formalizing and verifying mathematics using Lean4 has the potential to significantly transform future mathematical research practices. Furthermore, recent advancements include AI-driven automated theorem proving and the use of AI to tackle unsolved problems, marking a notable expansion of artificial intelligence into mathematical research. At this ZMC research conference, starting from computer formalization in arithmetic geometry and algebraic geometry, we aim to address AI-driven automated formalization and automated theorem proving from a mathematician&apos;s perspective. Similar to last year, this conference will also include a three-day group work session where participants will split into small groups and engage in formalizing mathematics related to arithmetic geometry using Lean4. Mathematicians whose specialties lie outside arithmetic geometry and algebraic geometry are also warmly welcome to attend! ---------- 【︎Session Content】: Morning sessions: Sessions featuring computer formalization, AI-driven automatic formalization, and automated theorem proving in arithmetic geometry Speakers: 　　Christian Merten (Utrecht) 　　Dagur Asgeirsson (Alberta) 　　Andrew Yang (Imperial College London) 　　Sho Sonoda (RIKEN AIP) 　　Kazumi Kasaura (Omron Sinic X) 　　Jiang Jiedong (Peking University) 　　Guoxiong Gao (Peking University) 　　...and more TBA Afternoon: Following a tutorial on computer formalization, we will conduct group work: Participants will be divided into several small groups to gain hands-on experience with computer formalization and work on the actual formalization of propositions and lemmas related to arithmetic geometry. We welcome your participation.

ZMC Conference 2026

ZEN数学センター（ZEN Mathematics Center; 略称 ZMC<a href="https://zen.ac.jp/zmc"> https://zen.ac.jp/zmc</a>）では、以下の研究集会を企画しております。 【タイトル】：Arithmetic geometry, AI, and Lean 【日程】：2025年7月21日（火）〜23日（木） 【開催地】：東京都中央区銀座4-12-15 歌舞伎座タワー12F ドワンゴセミナールーム 【オーガナイザー】： 　　Johan Commelin（Utrecht） 　　星裕一郎（京都大学数理解析研究所） 　　加藤文元（ZMC） 　　Kiran Kedlaya（UCSD） 　　Adam Topaz（Alberta） 【参加方法】：要予約、無料 【参加予約URL】： <a href="https://docs.google.com/forms/d/1YLTuuU5u3l4QGgR-X0BokQFL6UUUeYEsIxIaxDuyAWg/viewform?edit_requested=true">こちら</a>の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）を行います：参加者がいくつかの小グループに分かれて、実際に体験することでコンピューター形式化に入門し、数論幾何学の命題・補題などの実際の形式化に取り組みます。 皆様のご参加を歓迎致します。