数学系のためのLean勉強会

始め方

  1. VS Code, Git, Leanをインストールします。(参考: Leanのインストール
  2. ターミナル上でチュートリアルファイルを置きたいフォルダに移動して、以下のコマンドを実行します:
git clone https://github.com/yuma-mizuno/lean-math-workshop.git
cd lean-math-workshop
lake exe cache get
  1. VS Codeでlean-math-workshopフォルダを開きます。
  2. 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ディレクトリに変更を加える必要はありません。