団体トップページやコミュニティ

• Lean Theorem Prover Lean の公式サイト．
• Lean Community Lean のコミュニティ．
• Lean Prover Zulip Chat Lean について何でも質問できる公式のフォーラム．
• Lean 4 anarchy Lean のディスコードサーバ．Zulip と違って，くだけた雰囲気です．

ライブラリやツール

• Mathlib4 Lean で大学の学部程度の数学を実装したライブラリ．
• Lean4 VSCode 拡張機能 Lean4 のための VSCode 拡張機能．
• Loogle Mathlib の検索ツール．
• Moogle 自然言語で Mathlib から定理や定義が検索できるツール．
• Lean4 Web ブラウザ上で Lean が実行できるプレイグラウンド．

ドキュメントや教材など

• Theorem Proving in Lean 4 Lean 4の定理証明支援系としての側面に焦点を当てた公式チュートリアルテキストです．
• Lean Manual Lean 言語の公式ドキュメント．
• Functional Programming in Lean 関数型プログラミング言語としての Lean の入門書．
• Mathematics in Lean Lean でどのように数学を形式化するかを学ぶ教科書．初等整数論をはじめ，位相空間や測度も扱っています．
• Metaprogramming in Lean 4 Lean で独自のコマンドやタクティクを作るための方法を解説した本．
• Natural Number Game 4 Lean を使い，ペアノの公理から始めて自然数の基本的な性質を証明する初心者向けブラウザゲーム．
• Courses using Lean Lean を題材とした講義のリスト．

日本語リソース

• Theorem Proving in Lean 4 日本語訳 Theorem Proving in Lean 4 の有志による日本語訳です．
• Leanのインストール方法・elanとLakeの使い方 Leanのインストール方法・elanとLakeの使い方をまとめた有志による資料．
• 数学系のためのLean勉強会 2023/09/03 に開催された，数学ユーザに向けたLean言語の勉強会．資料が公開されています．
• Lean4 タクティク逆引きリスト 主なタクティクを使用場面から逆引きできるようにまとめたリストです．