[geometry-ml:05256] 数学系のためのLean勉強会 (9/3) 開催のお知らせ

[Taketo Sano]

幾何学 ML の皆様，

お世話になっております，理研の佐野岳人です．

定理証明支援系「Lean」に関するワークショップを下記の要領で開講するのでお知らせ致します．
対面またはオンラインでの参加を希望される方は下記のフォームよりご登録下さい．
本メールを重複して受け取られた方はどうぞご容赦ください．

---

日時: 2023年9月3日 (日) 10:00 - 17:30
会場: 新宿ビジネスルーム ／ Zoom
講師: 榎本 悠久（大阪公立大学），水野 勇磨（千葉大学）

題目: 数学系のためのLean勉強会

概要: 数学の理論や証明をコンピュータ上のプログラミング言語として実装する定理証明支援系というものが、近年注目を集めています。証明を定理証明支援系で形式化すると、誤りが無いことを保証できる上、証明がプログラムとして実装されることから、最近の生成AI（大規模言語モデル等）との組み合わせも期待されています。例えば、P. Scholze氏とD. Clausen氏のCondensed mathematicsの理論を証明支援系で実装するプロジェクトが昨年9月に完了しました。またLeanという証明支援系では学部レベルの数学の多くが実装されているライブラリがあり、学部レベルの数学は既にユーザーが自由に使うことができます。

本勉強会では、Leanを用いて、現代数学のユーザーである方々（数学の研究者や学生）を対象にし、プログラミング経験の無い方でも定理証明支援系を用いて数学を行うことができるようになることを目標としています。具体的には、勉強会参加者には自分のPCを持参してもらい、Leanをインストールするところからはじめ、純粋数学を専門としているオーガナイザーたちが用意したチュートリアル用演習問題に従って、普段の数学をどのようにプログラムとして再現するかの感覚を掴んでもらうことをねらいとしています。

参加登録: https://docs.google.com/forms/d/e/1FAIpQLScjIwo-VbJSA6nHNlvtZYKtXx1li8MuYaC3OL_NWlPQVXVpbw/viewform
申込締切: 前日(9月2日)まで．対面参加は定員30名に達した時点で締切．

詳細: https://haruhisa-enomoto.github.io/lean-math-workshop/

オーガナイザー:
・梅崎 直也（株式会社dwango/株式会社すうがくぶんか）
・榎本 悠久（大阪公立大学）
・佐野 岳人（理化学研究所 iTHEMS）
・水野 勇磨（千葉大学）

---

皆さまのご参加をお待ちしています．

Taketo SANO / 佐野岳人
Special Postdoctoral Researcher
iTHEMS, RIKEN, Japan.

https://taketo-sano.me/

-------------- next part --------------
HTMLの添付ファイルを保管しました...
URL: <https://mail.math.nagoya-u.ac.jp/pipermail/geometry-ml/attachments/20230721/a5f23e47/attachment.html>