「Lean」の版間の差分

2026年3月17日 (火) 01:13時点における最新版

証明支援系です。leanを用いて我々は定理とその証明を書くことができます。

Leanは「証明が正しいかどうかを判定する」こと、「どうすれば正しくなるかを提示する」ことで、証明の手助けを行います。

これを確認しながら、"Goals accomplished!" を見ることが目標のようです。

.lean ファイルを開くと自動で開かれる。

または、Lean 4 のメニューから Toggle InfoView を選択して開く。

@@ 1行目: / 1行目: @@
 https://lean-lang.org/
+証明支援系です。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
+=== 評価する ===
+<nowiki>#</nowiki>eval
+== 型 ==
+=== Prop ===
+命題
+== キーワード ==
+=== by ===
+=== fun ===
+=== intro ===
+=== exact ===