数学系のためのLean勉強会
始め方
- VS Code, Git, Leanをインストールします。（参考: Leanのインストール）
- ターミナル上でチュートリアルファイルを置きたいフォルダに移動して、以下のコマンドを実行します:
git clone https://github.com/yuma-mizuno/lean-math-workshop.git
cd lean-math-workshop
lake exe cache get
- VS Codeで
lean-math-workshopフォルダを開きます。 - VS Codeのエクスプローラーから、最初のレクチャーファイル
Tutorial/Basic/Lecture1.leanを開きます。
以上の手順を最初から初心者向けにまとめたYouTubeの動画：
内容
Tutorialフォルダの中に以下の教材が入っています。Solutionフォルダの中に入っているファイルは演習問題への解答を含みます。
Basic
Leanの基礎的な使い方や命題論理について
- Basic/Lecture1 命題論理
- Basic/Lecture2 mathlibの使い方
- Basic/Lecture3 任意と存在
- Basic/Lecture4 単射と全射
- Basic/Tactics 証明でよく使われるtacticについてのまとめ
Advanced/Analysis
実関数の微分等の解析からいくつかのトピック
- Advanced/Analysis/Lecture1 微分係数の定義および基本的な命題
- Advanced/Analysis/Lecture2 平均値の定理
- Advanced/Analysis/Lecture3 閉区間のコンパクト性
Advanced/Algebra
群論からいくつかのトピック
- Advanced/Algebra/Lecture1 群・部分群の定義と基本性質
- Advanced/Algebra/Lecture2 準同型の定義と基本性質
- Advanced/Algebra/Lecture3 群の集合への作用や同変写像
- Advanced/Algebra/Lecture4 左剰余類の集合、推移的
G集合の構造定理 - Advanced/Algebra/Lecture5 正規部分群・商群・準同型定理
Advanced/Category
圏論からいくつかのトピック
- Advanced/Category/Lecture1 圏の定義と例
- Advanced/Category/Lecture2 余極限の定義と例
参考書など
-
Theorem Proving in Lean 4は基礎的なことが詳しく書いてある教科書です。Leanで証明を書いていて知りたいことが出てきたらまずはこれを参考にすると良いです。日本語訳もあります。
-
A mathlib overviewでは、Leanの数学ライブラリmathlibで扱われている数学を概観できます。
-
Lean by Exampleは、Lean言語に関する日本語リファレンスです。定理証明をサポートするタクティクの紹介に加えて、各種コマンドも説明されています。初心者が調べるときに使いやすいよう、理論的な説明は最小限にとどめられ、コード例が豊富に紹介されています。
開発者向け情報
mk-exerciseというツールを用いて、Solutionディレクトリの内容からTutorialディレクトリの演習問題を自動的に生成しています。Solutionディレクトリに変更を加えても、それに合わせてTutorialディレクトリに変更を加える必要はありません。