「Lean」の版間の差分
ナビゲーションに移動
検索に移動
編集の要約なし |
編集の要約なし |
||
| (同じ利用者による、間の2版が非表示) | |||
| 6行目: | 6行目: | ||
== インストール == | == インストール == | ||
=== Leanをインストールする === | |||
https://lean-lang.org/install/ | https://lean-lang.org/install/ | ||
| 14行目: | 15行目: | ||
=== プロジェクトに Mathlib を導入する === | === プロジェクトに Mathlib を導入する === | ||
https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency | https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency | ||
lake exe cache get してビルド済みファイルをダウンロードしておきましょう。 | |||
その後 lean build を実行しておきましょう。 | |||
| 42行目: | 46行目: | ||
命題 | 命題 | ||
== | == 証明する == | ||
=== 構文 === | |||
==== := by ==== | |||
証明を開始します | |||
=== | === 定理や仮定を使う === | ||
=== | ==== rw [h] ==== | ||
h を使ってゴールを書き換えます | |||
==== intro h ==== | |||
前件(A→B においては A)を h という名前で導入します。 | |||
名前は何でもよく、前から順番に導入されるらしい。 | 名前は何でもよく、前から順番に導入されるらしい。 | ||
=== exact === | ==== exact h ==== | ||
先ほど導入したh: Aを除去して、A→B を導きます。 | |||
==== fun ==== | |||
=== 構成的証明 === | |||
==== exists A ==== | |||
∃を示すのに、これを満たすAを具体的に指定します | |||
== | == リンク集 == | ||
[https://lean-ja.github.io/lean-by-example/ Lean by Example] | |||
2026年5月22日 (金) 01:18時点における最新版
証明支援系です。leanを用いて我々は定理とその証明を書くことができます。
Leanは「証明が正しいかどうかを判定する」こと、「どうすれば正しくなるかを提示する」ことで、証明の手助けを行います。
インストール
Leanをインストールする
https://lean-lang.org/install/
- VSCode の拡張機能「Lean 4」をインストールする
- 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する
- プロジェクトが作られる。必要に応じて色々インストールされる。
プロジェクトに Mathlib を導入する
https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
lake exe cache get してビルド済みファイルをダウンロードしておきましょう。 その後 lean build を実行しておきましょう。
Lean InfoView
これを確認しながら、"Goals accomplished!" を見ることが目標のようです。
.lean ファイルを開くと自動で開かれる。
または、Lean 4 のメニューから Toggle InfoView を選択して開く。
やること
関数を定義する
def
定理を証明する
theorem
証明する（名前なし）
example
評価する
#eval
型
Prop
命題
証明する
構文
:= by
証明を開始します
定理や仮定を使う
rw [h]
h を使ってゴールを書き換えます
intro h
前件(A→B においては A)を h という名前で導入します。
名前は何でもよく、前から順番に導入されるらしい。
exact h
先ほど導入したh: Aを除去して、A→B を導きます。
fun
構成的証明
exists A
∃を示すのに、これを満たすAを具体的に指定します