AIと数学に関連する研究集会です。
各日、午前は招待講演、午後はグループワークを行います。
午前の講演では広くAIと数学に関連する内容で講演頂く予定です。午後のグループワークではAIを用いた数学研究を実践的に学ぶことを目標とします。
講演者
浅尾泰彦 (九州大学)
小池貴之 (筑波大学)
小泉淳之介 (理化学研究所)
佐藤玄基 (fcuro Inc.)
細野元気 (バーチャルキャスト)
洞龍弥 (ZEN大学)
三浦真人 (ファクトファクトリー)
宮﨑弘安 (NTTコミュニケーション科学基礎研究所)
グループワークについて：午後のグループワークでは少人数のグループに分かれてAIを用いた研究手法を実践的に習得することを目指します。具体的には以下のような目標を考えています。
(1) AIを用いて新たな定理の自然言語による証明を生成し、その証明をLeanで形式化する。
(2) AIを用いて既存の証明を整理簡略化し、そのLean形式化を与える。
(3) AIを用いた数学の研究方法や形式化に関連する技術の共有。
-- このグループワークの目的はAIを用いた数学研究の手法を学ぶことにあり、大量の証明を生成することにはありません。
得られた成果物の数学的内容の理解は集会後に時間をかけて各自が遂行し、発表する場合は著者が責任を持って論文を執筆することを推奨します。
-- AIやLeanを研究に利用したことがない方の参加も歓迎しています。
-- これは実験的な試みであり、世話人もAIやLeanの専門家ではありません。新しい数学の研究方法を参加者と共に模索したいと考えています。
グループワークへの参加にあたっては、生成AIの利用環境を各自が確保していることを前提としています。ChatGPT pro 相当が理想的ですが、例えばChatGPT plusやClaude proでも参加可能です。また事前にLeanをインストールしていただくことを推奨します。
利用可能な方は事前にeduroam登録をしていただけると助かります。
世話人：岩井雅崇(大阪大学)、松澤陽介(大阪公立大学)