リンク集

コミュニティ

  • Lean Theorem Prover Lean の公式サイト．
  • Lean Community Lean のユーザコミュニティ．
  • Lean Prover Zulip Chat Lean について何でも質問できる公式のフォーラム．
  • Lean 4 anarchy Lean のディスコードサーバ．Zulip と違って，くだけた雰囲気です．
  • Lean Forward 数学への Lean の応用を推進するコミュニティ．
  • lean-ja この資料を作っている lean-ja のディスコードサーバです.

ライブラリやツール

  • Mathlib4 Lean で大学の学部程度の数学を実装したライブラリ．
  • Lean4 VSCode 拡張機能 Lean4 のための VSCode 拡張機能．
  • Loogle Mathlib の検索ツール．
  • Moogle 自然言語で Mathlib から定理や定義が検索できるツール．
  • Chrome Lean Unicode Lean の VSCode 拡張機能が備える，Unicode 入力機能を Chrome で使えるようにする拡張機能．
  • Lean4 Web ブラウザ上で Lean が実行できるプレイグラウンド．
  • Reservoir 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 を題材とした講義のリスト．
  • Lean phrasebook 数学でのよくある推論ステップが，Lean にどのように翻訳されるかがよくまとめられたリストです．

日本語の資料