リンク集

Leanに関する有用なサイトへのリンク集です。

Lean 4

リンク集

• https://aconite-ac.github.io/: 有志個人様（下記Theorem Proving in Lean4の和訳者）がまとめてくださったリンク集

公式サイト・教科書的なもの

• Lean Theorem Prover: Lean全般の公式サイト
• Theorem Proving in Lean 4: 証明支援系としてのLeanの辞書・チュートリアルのようなもの
• Theorem Proving in Lean 4 日本語訳：上のテキストの有志による日本語訳。
• Lean 4 Manual: プログラミング言語としてのLeanのマニュアル
• mathlib4 (documentation): 有志による学部程度の数学をLean 4で実装するプロジェクト。今年7/16にLean 3から完全移行した。
• Lean Community: LeanやmathlibについてのLean公式コミュニティのページ。

実際に遊べる教材

• Natural Number Game: ペアノの公理から出発して自然数の性質を示すゲーム形式でLeanの基礎タクティクスを学べる（まだ開発中で説明不足な点などあり）
• Mathematics in Lean, GitHubリポジトリ：学部数学程度をLeanで学べる教材。

全般

• Xena project: 数学者のKevin Buzzard氏が運営する、現代数学とLean等による形式化についてのブログ。特に以下の記事は数学系の人たちへ有用。
  • Mathematics in type theory.: 数学者向けに、型理論を用いた数学の定式化を解説した記事
• Lean Prover Zulip Chat: Leanに関することが何でも質問したり議論したりできる掲示板のようなもの。

Lean 3

現在LeanコミュニティはLean 3からLean 4への移行期であり、現在からLean 3を使うのは特別な理由がない限りはあまり勧められない。

• mathlib (documentation): mathlib 4 の前身である Lean 3 で書かれた数学ライブラリ。