次のステップ

本書は、ごくわずかの対話的定理証明を含めたLeanによる関数型プログラミングのごく基本的なことについて紹介しています。Leanのような依存型関数型言語の使用は深いトピックであり、語るべきことはまだまだあります。読者の興味に応じて、以下のリソースがLean4の学習に役立つでしょう。

Lean自体の学習

Lean4そのものについては以下のリソースで記述されています：

• Theorem Proving in Lean 4 はLeanで証明を書くためのチュートリアルです。¹
• The Lean 4 Manual はLean言語とその機能のリファレンスを提供しています。本書執筆時点ではまだ不完全ですが、本書よりもLeanの多くの側面が詳細に記述されています。
• How To Prove It With Lean は How To Prove It という定評のある教科書のLeanベースの付録であり、紙と鉛筆で数学的証明を書くための入門書です。
• Metaprogramming in Lean 4 は中置演算子や記法などからマクロ・カスタムのタクティク・完全にカスタムな組み込み言語まで、Leanの拡張メカニズムの概要を提供しています。
• Functional Programming in Lean は再帰に関するジョークが好きな読者には面白いかもしれません。 ²

しかし、Leanを学び続ける最善の方法はコードを読み、実際に書いてみて、行き詰った時にはドキュメントを参照することです。さらに、Lean Zulip はほかのLeanユーザに会ったり、助けを求めたり、他の人を助けたりするのに最適な場所です。

標準ライブラリ

いざふたを開けてみると、Lean自体にはかなり最小限のライブラリしか含まれていません。Leanはセルフホスティッドであり、含まれているコードはLean自身を十分実装しうるものです。多くのアプリケーションではより大きな標準ライブラリが必要です。

batteries ³ は現在進行形で開発されている標準ライブラリであり、Leanのコンパイラ自体のスコープから外れた多くのデータ構造・タクティク・型クラスのインスタンス・関数を保持しています。batteries を使用するにはまず、使用しているLean4のバージョンと互換性のあるコミットを探します（つまり、lean-toolchain ファイルが読者のプロジェクトのものと一致するものです）。次に、lakefile.lean のトップレベルに以下を追加します。ここで COMMIT_HASH は適切なバージョンを指します：

require batteries from git
  "https://github.com/leanprover-community/batteries" @ "COMMIT_HASH"

Leanによる数学

数学者のためのリソースのほとんどはLean3用に書かれています。コミュニティサイト では幅広い分野があります。Lean4で数学を始めるには、数学ライブラリ mathlib をLean3からLean4に移植するプロセスに参加することが一番簡単でしょう。詳しくは mathlib4 README を参照してください。

計算機科学における依存型の利用

CoqはLeanと多くの共通点を持つ言語です。計算機科学者にとっては対話的な教科書 Software Foundations シリーズは計算機科学におけるCoqの応用について優れた入門書を提供しています。LeanとCoqの基本的な考え方は非常に似ており、言語に対するスキルはシステム間で容易に移行可能です。

依存型によるプログラミング

プログラムを構造化するために添字族と依存型を使うことを学びたいと思っているプログラマにとって、Edwin Bradyの Type Driven Development with Idris は素晴らしい入門書となります。Coqと同様、IdrisはLeanの親戚ですが、タクティクはありません。

依存型の理解

The Little Typer は論理学やプログラミング言語の理論を正式に学んだことはないが、依存型理論の核となる考え方について理解を深めたいと考えているプログラマのための本です。上記のすべてのリソースが可能な限り実用的であることを目指しているのに対し、The Little Typer はプログラミングの概念のみを用いて0から基本を構築する依存型理論へのアプローチを提示しています。免責事項：Functional Programming in Lean の著者は The Little Typer の著者でもあります。