Lean by Example

プログラミング言語であるとともに定理証明支援系でもある Lean 言語と、その主要なライブラリの使い方を豊富なコード例とともに解説した資料です。

本書が気に入ったら、ぜひ GitHub からスター🌟をつけてください。

本書の特色 😎

1. 内容が正確

Lean は開発が活発に続いているソフトウェアであり、毎月のように新しいリリースが行われています。その際破壊的な変更が行われることは少なくありません。変更によって古くなってしまった記述を自動的に見つける方法がなければ、内容の信頼性が損なわれます。

本書では、記述内容を可能な限りコードとして表現することにより、「ビルドが通れば記述内容は正しい」という状態を維持しています。さらに、内容を更新するごとにビルドが自動的に走るように設定してあります。これにより本書のほぼすべての記述はバージョン leanprover/lean4:v4.14.0-rc2 で実際に間違いがないということを確認済みです。

間違った記述を見つけられた際はお手数ですが issue でご報告をお願いします。

2. 情報が新しい

本書には、Lean とそのライブラリのバージョンを自動で更新するワークフローが設定されており、定期的にバージョンを最新のものに更新しています。Lean の最新情報をすべて掲載することはかないませんが、最新の情報を提供できるよう努めています。

3. コードをすぐに試せる

本書のすべての Lean コードブロックは、マウスを重ねると Lean Playground へジャンプするボタン が現れるようになっています。

またコードブロックの中には、import 文が足りないなどの理由でそのままでは実行できないものがありますが、そうした場合は画面右上の実行ボタン をクリックしていただければ、ファイル全体を実行することができます。

スポンサー

このプロジェクトは Proxima Technology 様よりご支援を頂いています。

Proxima Technology（プロキシマテクノロジー）は数学の社会実装を目指し、その⼀環としてモデル予測制御の民主化を掲げているAIスタートアップ企業です。数理科学の力で社会を変えることを企業の使命としています。