「Lean」の版間の差分
ナビゲーションに移動
検索に移動
編集の要約なし |
編集の要約なし |
||
| 1行目: | 1行目: | ||
https://lean-lang.org/ | https://lean-lang.org/ | ||
証明支援系です。leanを用いて我々は定理とその証明を書くことができます。 | |||
Leanは「証明が正しいかどうかを判定する」こと、「どうすれば正しくなるかを提示する」ことで、証明の手助けを行います。 | |||
== インストール == | == インストール == | ||
| 25行目: | 29行目: | ||
=== 評価する === | === 評価する === | ||
<nowiki>#</nowiki>eval | <nowiki>#</nowiki>eval | ||
== 型 == | |||
=== Prop === | |||
命題 | |||
== キーワード == | |||
=== by === | |||
=== fun === | |||
=== intro === | |||
=== exact === | |||
2026年3月17日 (火) 01:05時点における版
証明支援系です。leanを用いて我々は定理とその証明を書くことができます。
Leanは「証明が正しいかどうかを判定する」こと、「どうすれば正しくなるかを提示する」ことで、証明の手助けを行います。
インストール
https://lean-lang.org/install/
- VSCode の拡張機能「Lean 4」をインストールする
- 適当にファイルを開き、右上のメニューから Lean 4 > New Project... を選択する
- プロジェクトが作られる。必要に応じて色々インストールされる。
Lean InfoView
これを確認するのが目的？
.lean ファイルを開くと自動で開かれる。
または、Lean 4 のメニューから Toggle InfoView を選択して開く。
やること
関数を定義する
def
定理を証明する
theorem
評価する
#eval
型
Prop
命題