For the LANA Project Announcement

LANA プロジェクト発表にあたって

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）を行います：参加者がいくつかの小グループに分かれて、実際に体験することでコンピューター形式化に入門し、数論幾何学の命題・補題などの実際の形式化に取り組みます。 皆様のご参加を歓迎致します。

ZMC カンファレンス 2026 開催のお知らせ

The ZEN Mathematics Center (ZMC) is pleased to announce the upcoming research conference detailed below. We look forward to welcoming interested participants.・As venue capacity is limited, we kindly request those wishing to attend to notify Fumihito Kato (<a href="mailto:fumiharu_kato@zen.ac.jp" target="_blank" rel="noopener noreferrer nofollow">fumiharu_kato@zen.ac.jp</a>).＝＝＝＝＝＝＝＝＝＝ ZMC &amp; NTT-IFM Joint Seminar・Date: Wednesday, October 22, Afternoon ・Location: ZEN University Zushi Campus 3-12-11 Shinjuku, Zushi City, Kanagawa Prefecture 15-minute walk from JR Yokosuka Line “Zushi” Station13:00〜13:30 Fumiharu Kato (ZEN university / ZMC） 13:40〜14:10 Masato Wakayama (ZEN university &amp; NTT-IFM） 14:40〜15:40 Zeev Rudnick (Tel-Aviv university) 16:00〜17:00 Shai Haran (Technion)Speaker: Fumiharu Kato (ZEN university / ZMC） Title: Sharp bounds for the number of rational points on algebraic curves and dimension growth over all global fields Abstract: Joint work with Gal Binyamini (Weizmann) &amp; Raf Cluckers (Lille). I will talk on our recent results on the bounds of K-rational points, where K is a number field, of height at most H on hyper surfaces X of degree d. In many cases, our bounds depends quadratically on d with the optimal exponents of H, which leads to new results on Heath-Brown&apos;s and Serre&apos;s dimension growth conjecture for global fields. I will also mention on analogous results for global fields in positive characteristic. The proofs are given by the p-adic determinant method, and the optimal dependence on d is achieved using a technical improvement in the treatment of high multiplicity points on mod p reductions of algebraic curves.Speaker: Masato Wakayama (ZEN university &amp; NTT-IFM） Title: Light-matter interactions and number theory Abstract: The quantum Rabi model (QRM) describes the coupling of a two-state system to a bosonic field mode. There are also several imporatnat related/generalized models such as the asymmetric QRM, two photon QRM, quantum Rabi-Stark models, which describe the fundamental mechanism of light-matter interaction. In this talk, we introduce mathematical challenges, particularly number theoretic ones, that arise from the study of the spectrum (energy states) of the target Hamiltonian that describes such quantum interactions, along with several conjectures.Speaker: Zeev Rudnick (Tel Aviv University) Title: Number theory and spectral theory of the Laplacian Abstract: I will discuss some of the interactions between number theory and the spectral theory of the Laplacian. Some have very classical background, such as the connection with lattice point problems. Others are newer, including connections between random matrix theory, the zeros of the Riemann zeta function, and spectral statistics on the moduli space of hyperbolic surfaces.Speaker: Shai Haran (Technion) Title: Non additive geometry Abstract: The usual dictionary between geometry and commutative algebra is not appropriate for Arithmetic geometry because addition is a singular operation at the &quot;Real prime&quot;. We replace Rings, with addition and multiplication, by Props (=strict symmetric monoidal category generated by one object), or by Bioperad (=two closed symmetric operads acting on each other): to a ring we associate the prop of all matrices over it, with matrix multiplication and block direct sums as the basic operations, or the bioperad consisting of all raw and column vectors over it. We define the &quot;commutative&quot; props and bioperads, and using them we develop a generalized algebraic geometry, following Grothendieck footsteps closely. This new geometry is appropriate for Arithmetic (and potentially also for Physics).

ZMC&NTT-IFM  Joint Seminar

ZEN数学センター（ZMC）では、下記の研究集会の開催を予定しております。ご興味ある方のご参加をお待ちしております。・会場の収容に限りがございますので、参加を希望される方は、お手数ではございますが、加藤文元（<a href="mailto:fumiharu_kato@zen.ac.jp" target="_blank" rel="noopener noreferrer nofollow">fumiharu_kato@zen.ac.jp</a>）までご一報ください。＝＝＝＝＝＝＝＝＝＝ ZMC&amp;NTT-IFM合同セミナー・日程：10月22日（水）午後 ・場所：ZEN大学逗子キャンパス 　神奈川県逗子市新宿3丁目12-11 　JR横須賀線「逗子」駅より徒歩15分13:00〜13:30 Fumiharu Kato (ZEN university / ZMC）13:40〜14:10 Masato Wakayama (ZEN university &amp; NTT-IFM） 14:40〜15:40 Zeev Rudnick (Tel-Aviv university) 16:00〜17:00 Shai Haran (Technion)Speaker: Fumiharu Kato (ZEN university / ZMC） Title: Sharp bounds for the number of rational points on algebraic curves and dimension growth over all global fields Abstract: Joint work with Gal Binyamini (Weizmann) &amp; Raf Cluckers (Lille). I will talk on our recent results on the bounds of K-rational points, where K is a number field, of height at most H on hyper surfaces X of degree d. In many cases, our bounds depends quadratically on d with the optimal exponents of H, which leads to new results on Heath-Brown&apos;s and Serre&apos;s dimension growth conjecture for global fields. I will also mention on analogous results for global fields in positive characteristic. The proofs are given by the p-adic determinant method, and the optimal dependence on d is achieved using a technical improvement in the treatment of high multiplicity points on mod p reductions of algebraic curves.Speaker: Masato Wakayama (ZEN university &amp; NTT-IFM） Title: Light-matter interactions and number theory Abstract: The quantum Rabi model (QRM) describes the coupling of a two-state system to a bosonic field mode. There are also several imporatnat related/generalized models such as the asymmetric QRM, two photon QRM, quantum Rabi-Stark models, which describe the fundamental mechanism of light-matter interaction. In this talk, we introduce mathematical challenges, particularly number theoretic ones, that arise from the study of the spectrum (energy states) of the target Hamiltonian that describes such quantum interactions, along with several conjectures.Speaker: Zeev Rudnick (Tel Aviv University) Title: Number theory and spectral theory of the Laplacian Abstract: I will discuss some of the interactions between number theory and the spectral theory of the Laplacian. Some have very classical background, such as the connection with lattice point problems. Others are newer, including connections between random matrix theory, the zeros of the Riemann zeta function, and spectral statistics on the moduli space of hyperbolic surfaces.Speaker: Shai Haran (Technion) Title: Non additive geometry Abstract: The usual dictionary between geometry and commutative algebra is not appropriate for Arithmetic geometry because addition is a singular operation at the &quot;Real prime&quot;. We replace Rings, with addition and multiplication, by Props (=strict symmetric monoidal category generated by one object), or by Bioperad (=two closed symmetric operads acting on each other): to a ring we associate the prop of all matrices over it, with matrix multiplication and block direct sums as the basic operations, or the bioperad consisting of all raw and column vectors over it. We define the &quot;commutative&quot; props and bioperads, and using them we develop a generalized algebraic geometry, following Grothendieck footsteps closely. This new geometry is appropriate for Arithmetic (and potentially also for Physics).

ZMC&NTT-IFM合同セミナー

<ul><li>Conference Name: ZMC Conference 2025</li><li>Title: Anabelian Geometry and its Computer Formalization</li><li>Dates: July 1 - July 4, 2025</li><li>Venue: Floor 12, Dwango Seminar Room, KABUKIZA TOWER, 4-12-15 Ginza, Chuo-ku, Tokyo, 104-0061 JAPAN</li><li>Organizers:<ul><li>Johan Commelin (Utrecht)</li><li>Yuichiro Hoshi (RIMS, Kyoto)</li><li>Fumiharu Kato (ZMC)</li><li>Kiran Kedlaya (UCSD)</li><li>Adam Topaz (Alberta)</li></ul></li><li>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.</li><li>Participation: Reservation required, free</li><li>Reservation: click here（<a href="https://docs.google.com/forms/d/e/1FAIpQLSd7Jg4PWJ-RATxazSjwc2cj3W1lY2iaS1-YSwn7Hbw6bliIvg/viewform?usp=dialog）">https://docs.google.com/forms/d/e/1FAIpQLSd7Jg4PWJ-RATxazSjwc2cj3W1lY2iaS1-YSwn7Hbw6bliIvg/viewform?usp=dialog）</a></li></ul>

ZMC Conference 2025

<ul><li>Conference Name: ZMC Conference 2025</li><li>Title: Anabelian Geometry and its Computer Formalization</li><li>Dates: July 1 - July 4, 2025</li><li>Venue: Floor 12, Dwango Seminar Room, KABUKIZA TOWER, 4-12-15 Ginza, Chuo-ku, Tokyo, 104-0061 JAPAN</li><li>Organizers:<ul><li>Johan Commelin (Utrecht)</li><li>Yuichiro Hoshi (RIMS, Kyoto)</li><li>Fumiharu Kato (ZMC)</li><li>Kiran Kedlaya (UCSD)</li><li>Adam Topaz (Alberta)</li></ul></li><li>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.</li><li>Participation: Reservation required, free</li><li>Reservation:<a href="https://docs.google.com/forms/d/e/1FAIpQLSd7Jg4PWJ-RATxazSjwc2cj3W1lY2iaS1-YSwn7Hbw6bliIvg/viewform?usp=dialog" target="_blank" rel="noopener noreferrer nofollow"> click here</a></li></ul>

ZMCカンファレンス2025 開催のお知らせ

Upon the approval of ZEN University, the former IUGC was renamed ZEN Mathematics Center (ZMC). The ZMC will be managed by the following organization. •   Director: Fumiharu Kato •   Deputy Director: Ivan Fesenko •   Administrative Staff: Akiko Takagi •   Technical Staff: Daisuke Seshita, Toshihiko Nakazawa

Announcement of name change to ZEN Mathematics Center (ZMC)

2024年11月12日（火）、旧IUGCはZEN数学センター（ZEN Mathematics Center）と改称しました。 今後、以下の体制で運営していきます。<ul><li>所長：加藤 文元</li><li>副所長：イヴァン・フェセンコ</li><li>事務スタッフ：高木 章子</li><li>テクニカルスタッフ：瀬下 大輔、中澤俊彦</li></ul>

TOPICS

LANA プロジェクト発表にあたって

ZMC カンファレンス 2026 開催のお知らせ

ZMC&NTT-IFM合同セミナー

ZMCカンファレンス2025 開催のお知らせ

ZEN数学センター（ZMC）へ改称のお知らせ