Lean
ナビゲーションに移動
検索に移動
証明支援系です。leanを用いて我々は定理とその証明を書くことができます。
Leanは「証明が正しいかどうかを判定する」こと、「どうすれば正しくなるかを提示する」ことで、証明の手助けを行います。
インストール
https://lean-lang.org/install/
- VSCode の拡張機能「Lean 4」をインストールする
- 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する
- プロジェクトが作られる。必要に応じて色々インストールされる。
Lean InfoView
これを確認しながら、"Goals accomplished!" を見ることが目標のようです。
.lean ファイルを開くと自動で開かれる。
または、Lean 4 のメニューから Toggle InfoView を選択して開く。
やること
関数を定義する
def
定理を証明する
theorem
証明する（名前なし）
example
評価する
#eval
型
Prop
命題
キーワード
by
「タクティク」によって証明を開始します
intro
intro h
のように書くと、前件(A→B においては A)を h という名前で導入します。
名前は何でもよく、前から順番に導入されるらしい。
exact
exact h と書くと先ほど導入したh : Aを除去して、A→B を導きます。