# リンク集

## 🌐 コミュニティ

* [Lean Theorem Prover](https://leanprover.github.io/) Lean の公式サイト。
* [Lean Community](https://leanprover-community.github.io/) Lean のユーザコミュニティ。
* [Lean Prover Zulip Chat](https://leanprover.zulipchat.com/) Lean について何でも質問できる公式のフォーラム。
* [Lean 4 anarchy](https://discord.com/invite/WZ9bs9UCvx) Lean のディスコードサーバ。Zulip と違って、くだけた雰囲気です。
* [Lean Forward](https://lean-forward.github.io/) 数学への Lean の応用を推進するコミュニティ。
* [lean-ja](https://discord.gg/p32ZfnVawh) この資料を作っている lean-ja のディスコードサーバです。

## 📰 ブログ

* [Lean Blog](https://lean-lang.org/blog/) Lean の公式ブログ。各リリースにおける新機能が説明されていたり、ロードマップについて書かれていたりします。
* [Lean community blog](https://leanprover-community.github.io/blog/) Lean コミュニティが運営するブログ。Lean での数学の形式化プロジェクトに関する話題が多いです。

## 🧰 ライブラリやツール

* [Mathlib4](https://github.com/leanprover-community/mathlib4) Lean で大学の学部程度の数学を実装したライブラリ。
* [Lean4 VSCode 拡張機能](https://github.com/leanprover/vscode-lean4) Lean4 のための VSCode 拡張機能。
* [Loogle](https://loogle.lean-lang.org/) Mathlib の検索ツール。型の情報や定数名から検索ができます。vscode-lean4 から実行することもできます。
* [Moogle](https://www.moogle.ai/) 自然言語で Mathlib から定理や定義が検索できるサイト。VSCode 拡張機能もあります。
* [Lean Search](https://leansearch.net/) 自然言語で Mathlib から定理や定義が検索できるサイト。これに関連して[「A Semantic Search Engine for Mathlib4」](https://www.semanticscholar.org/paper/A-Semantic-Search-Engine-for-Mathlib4-Gao-Ju/da6bf364987a605843d56b19f9d0b1546b192c5f?utm_source=direct_link)という論文があります。
* [Lean4 Web](https://live.lean-lang.org/) ブラウザ上で Lean が実行できるプレイグラウンド。
* [Reservoir](https://reservoir.lean-lang.org/) Lean 公式のパッケージレジストリ。

## 📖 書籍

* [Theorem Proving in Lean 4](https://leanprover.github.io/theorem_proving_in_lean4) Lean 4の定理証明支援系としての側面に焦点を当てた公式チュートリアルテキストです。理論的な記述が多めです。
* [Lean Manual](https://lean-lang.org/lean4/doc/) Lean 言語の公式ドキュメント。執筆中であり欠けている個所がいくつもあります。
* [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/) 関数型プログラミング言語としての Lean の入門書。
* [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/) Lean で数学を形式化する方法を学ぶ教科書。初等整数論をはじめ、位相空間論や測度論も扱われるなど内容が充実しており、多くの演習問題があります。
* [Metaprogramming in Lean 4](https://leanprover-community.github.io/lean4-metaprogramming-book/) Lean で独自のコマンドやタクティクを作る方法を解説した本。
* [The Mechanics of Proof](https://hrmacbeth.github.io/math2001/) 大学の初級レベルの授業のための Lean を使った教科書。Mathlib にはない独自のタクティクが使用されていることに注意が必要です。
* [The Hitchhiker's Guide to Logical Verification](https://github.com/blanchette/interactive_theorem_proving_2024) 「	Formal Proof and Verification」という授業の参考書。テーマは形式検証であり、形式数学の形式化だけでなくプログラミング意味論にも触れています。

## 📝 書籍以外の参考資料

* [Lean phrasebook](https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0) 数学でのよくある推論ステップが、Lean にどのように翻訳されるかがよくまとめられたリストです。
* [Natural Number Game 4](https://adam.math.hhu.de/#/g/leanprover-community/NNG4) Lean を使い、ペアノの公理から始めて自然数の基本的な性質を証明する初心者向けブラウザゲーム。
* [Courses using Lean](https://leanprover-community.github.io/teaching/courses.html) Lean を題材とした講義のリスト。

## 🗾 日本語の資料

* [Theorem Proving in Lean 4 日本語訳](https://aconite-ac.github.io/theorem_proving_in_lean4_ja/) Lean で数学の証明を行う方法を解説した公式チュートリアルの、有志による日本語訳です。
* [数学系のためのLean勉強会](https://github.com/yuma-mizuno/lean-math-workshop) Lean で数学をどのように実装するのか、実際に実装する過程を追うことで学べる教材です。
* [Leanのインストール方法・elanとLakeの使い方](https://aconite-ac.github.io/how_to_install_lean/) Leanのインストール方法・elanとLakeの使い方をまとめた有志による資料。