aconite-ac.github.io

このサイトについて

Leanの日本語情報(非公式)を掲載します。

Theorem Proving in Lean 4 日本語訳 : Leanのチュートリアルドキュメント「Theorem Proving in Lean 4」の非公式日本語訳です。
Leanのインストール方法・elanとLakeの使い方 : Leanのインストール方法・elanとLakeの使い方をまとめた非公式資料です。

Lean Theorem Prover : 定理証明支援系「Lean」の公式サイトです。
Theorem Proving in Lean 4 : Lean 4の定理証明支援系としての側面に焦点を当てた公式チュートリアルテキストです。
Functional Programming in Lean : Lean 4のプログラミング言語としての側面に焦点を当てた公式チュートリアルテキストです。
Lean Manual : Lean 4のマニュアルですが、一部未完成です。
lean4-samples : Lean 4で書かれたサンプルプログラム集です。Hello World Sample、Guess My Number、Rubik's cube visualiserなどがあります。

Lean Community : Leanの数学ライブラリ「mathlib」の開発やLeanに関するドキュメンテーションの作成をしているユーザーコミュニティ「Lean community」のサイトです。
Mathlib4 : Lean communityによって開発が進められているLean 4向け数学ライブラリです。
Mathlib4 Documentation : Mathlib4のドキュメンテーションです。
Natural Number Game 4 : オンラインで動作する、ゲーム形式で自然数に関する定理を証明しながらLean 4を学ぶチュートリアルです。
Lean学習初めの一歩に最適ですが、開発途中で、タクティクの説明が見れない、Inequality Worldが実装されていないなど不便な点もあります。
Natural Number Game 3 : 上記のLean 3版です。Natural Number Game 4の開発が完了するまではこちらで遊ぶのもいいでしょう。
Lean 4に移行する際は、reflではなくrflと書くこと、各タクティクの末尾に,を付ける必要はないこと、rw hではなくrw [h]と書くことなどに気を付けましょう。
Mathematics in Lean : 論理・集合から測度論・微積分までの数学の定理を実際に形式化しながらLean 4を学ぶテキストです。