数学系のためのLean勉強会

会場

東京都新宿区西新宿7-4-4 武蔵ビル6F
アクセス
Google Map

日時

2023年9月3日（日） 10:00-

概要

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

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

前提知識

数学科の学部二年程度の内容には習熟していることを前提とします。

スケジュール

時間	内容
10:00 - 10:15	イントロダクション（水野）
10:15 - 10:45	Leanの基礎（榎本）
11:00 - 12:30	チュートリアル基礎
14:00 - 16:30	チュートリアル実践
16:30 - 17:30	フリーディスカッション

基礎を講師の二人が話した後は、基本的にはすべてみなさんに演習の授業のようにLeanの教材に取り組んでもらい、slack等で講師や人々と質疑応答する、という形式で行いました。

教材

https://github.com/yuma-mizuno/lean-math-workshop

スライド

教材を開くまでの準備の解説動画

VS Code, Lean, Gitをインストールして、上の教材を自分のPCにダウンロードして遊べるようになるまでの、初心者向け解説動画です。