Blog

Leanには強力な数学用ライブラリ Mathlib がありますが，これを利用するためには，プロジェクトディレクトリを作成する必要があります．この記事では，Lean 4における数学用ライブラリ Mathlib を使った証明プログラムを書くためのプロジェクトディレクトリの作成方法を述べます．Leanプロジェクトの作り方のページに書かれている手順に従い，プロジェクトを作成した記録を以下に述べます．また，すでにLean4をインストールされていることを想定していますので，Lean4自体のインストール手順については触れません． 作業は M1 Mac 上で実施しました．Lean のインストールはvscodeの拡張機能である lean4 を用いて行っています． 参考リンクに従い作業を進めてみる．．． vscode をインストールすると，Leanプロジェクト管理ツールである，elan が ~/.elan/bin/にインストールされていますので，以下のコマンドでツールをアップデートします． $ elan update info: syncing channel updates for ‘stable’ info: latest update on stable, lean version v4.0.0-m5 info: downloading component ‘lean’ Total: 124.9 MiB Speed: 1.5 MiB/s info: installing component ‘lean’ info: syncing channel updates for ‘nightly’…

数学系のためのLean勉強会の教材 Tutorial/Basic/Lecture1 を解いてみた． Basic/Lecture1.lean import Std /- # 遊び方 -/ — 証明があるべき場所に`sorry`と書いてあるので… example : 1 + 1 = 2 := by sorry — 正しい証明に書き直そう！ example : 1 + 1 = 2 := by triv /- # Leanにおける論理 数学的に意味のある文を**命題**と呼ぶ。例えば、「1 + 1 = 2」「3は偶数である」「リーマン予想」などが 命題である。命題は真である場合もあれば偽である場合もあるし、真偽がわかっていない場合もある。数学の 教科書などでは「命題」という単語は「定理」という単語の別名として使われることもあるが、ここでは違う 意味で使われていることに注意しよう。 `P`が命題であることをLeanでは`P : Prop`と書く。また、`h : P`と書けば`h`が`P`の証明であることを 意味する。別の言い方をすると、`h : P`は`P`が真であり、その事実に`h`と名前を付けているという こともできる。 -/…

千葉大学 萩原先生の 応用情報数理学特論　第０３回 の演習をLean4で写経してみる． 演習03-01 — 目標1. section — section は変数のスコープをつけるもの． variable (A B : Prop) section variable (a : A) example : A := a example : (A → B) → B := fun (f : A → B) => f a end section variable (h : A ∧ B) — ここからは A ∧…

千葉大学 萩原先生の 応用情報数理学特論　第０２回 の演習をLean4で写経してみる． 演習02-01 — 目標１．example — 目標２．show, from variable (A B : Prop) variable (h : A ∧ B) — example : 証明を与えられる命題 := 証明の具体例 example : A := And.left h — A の証明を与えているイメージ example : B := h.right — B の証明を与えているイメージ example : B ∧ A := And.intro (h.right) (h.left) example :…

Lean による定理証明に関する素振り． 今回は次の命題を証明する． 命題 P → R を証明するための仮定として h : P → Q と，h’ : Q → R が与えられているが，命題 P の証明は仮定として与えられていない． この状態で h’ : Q → R を適用すると， このようなエラー表示が出てしまい，証明が進まない． 命題 P の証明が足りていないので，intro を使って apply h’ より前に仮定を追加する． intro (hP : P) は intro hP だけでもよい（Leanが忖度してくれる）． 続けて順に仮定を適用することで No goals となる．これで証明完了． なお，短く書くと次のようにも書ける． example (h : P → Q)…

Lean による定理証明に関する素振り． 今回は次の命題を証明する． ⊢ の右側に表示されている現在証明すべき命題は Q ．まず，仮定 h : P → Q を適用すると， ⊢ の右側に P が表示される． 続けて，仮定 hP : P を適用すると， No goals となる．これで証明完了． なお，2つの仮定の適用は次のように1行にまとめることもできる． example (h : P → Q) (hP : P) : Q := by apply h hP

Lean による定理証明に関する素振り． vscode上でLeanをインストールすれば，下記のように拡張子が .lean のファイルを開くとvscodeがLeanモードになる． Leanモードでは，サイドビューに定理証明の状況が表示される． 以下のように証明したい命題を example として定義し，by 以降に証明を書く．このモードを tactic mode という． この状態で exampleの次の行へカーソルを移動させると，サイドビューに証明の状況が表示され，現在証明すべき命題が ⊢ の右側に表示される．P である． 命題 P の証明 hP があるので，apply hP とすれば証明完了． サイドビューの Tactic state が変化し，No goals となる．これで証明完了（らしい）．

千葉大学 萩原先生の 応用情報数理学特論　第０１回 の演習をLean4で写経してみる． 演習01-01 割愛 m(_ _)m 演習01-02 variable (A : Type) variable (B C D: Type) variable (a : A) variable (b₁ b₂ : B) variable (c : C) variable (f : A → B) variable (g : B → C) variable (h : A → B → C → D) variable (i…