役立つLeanのリソース

Leanをマスターするのに役立つリソース集

  • 公式サイトは、この言語に関する情報の中心となるリポジトリです。何もインストールせずに言語を試せるオンラインのプレイグラウンドもあります。
  • Reservoirは、LeanとLakeのエコシステムにあるパッケージのインデックスを作成し、ビルドとテストを行います。サードパーティ製パッケージを探すならここです。
  • Lean Communityは、Leanのエコシステムを中心とした協働的なオープンソースのネットワークです。コミュニティ主導のLean 4向け数学ライブラリである_mathlib_を担っています。
  • Lean 4 Zulip Chatは、Lean Communityの主要なチャットです。