まあ もう、勝負ついたでしょ
下記 ZMCカンファレンス2025 遠アーベル幾何学とそのコンピュータ形式化で
ご注目は、Kiran Kedlaya（UCSD）
かれが、星裕一郎と加藤文元の側に立ったってことよ

(参考)
https://zen.ac.jp/zmc/activities/conf2025
zen.ac
ZMCカンファレンス2025
遠アーベル幾何学とそのコンピュータ形式化
日程：2025年7月1日（火）〜4日（金）
開催地：東京都中央区銀座4-12-15 歌舞伎座タワー12F ドワンゴセミナールーム

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

会議のテーマ：
近年、コンピュータによる数学の形式化に興味を持つ人が増えており、Lean4による数学の形式化と検証が、将来の数学研究のやり方を大きく変える可能性があると認識されつつあります。これらの形式化は、すでに数論幾何学のさまざまな分野に応用されていますが、今回の研究集会では、遠アーベル幾何学のLean4による形式化の可能性について議論したいと思います。
本会議では、遠アーベル幾何学に関する最新の研究発表だけでなく、遠アーベル幾何学に関連するライブラリの構築についても議論したいと思います。
また、小グループに分かれて、実際にLean4を用いて遠アーベル幾何学に関連する数学の形式化に取り組む予定と、機械学習による自動形式化に関するセッションも予定されています。