# リンク集

## コミュニティ

* [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 のディスコードサーバです.

## ライブラリやツール

* [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 の検索ツール．
* [Moogle](https://www.moogle.ai/) 自然言語で Mathlib から定理や定義が検索できるツール．
* [Chrome Lean Unicode](https://github.com/arthurpaulino/chrome-lean-unicode) Lean の VSCode 拡張機能が備える，Unicode 入力機能を Chrome で使えるようにする拡張機能．
* [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 で独自のコマンドやタクティクを作るための方法を解説した本．
* [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 を題材とした講義のリスト．
* [Lean phrasebook](https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0) 数学でのよくある推論ステップが，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の使い方をまとめた有志による資料．