Lean by Example

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

この文書は lean-ja が管理しています．誤りのご指摘，ご提案などは GitHub リポジトリからお願いします．

lean-ja の Discord サーバがこちらにあります．質問や相談などはこちらにどうぞ．

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

本書の特色 😎

1. 内容が正確

本書のすべての Lean コードブロックはバージョン leanprover/lean4:v4.9.0 で実際にエラーなく動くことを CI で確認しています．動かないコード例を見つけられた際はお手数ですが issue でご報告をお願いします．

2. 情報が新しい

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

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

本書のすべての Lean コードブロックは，マウスを重ねると Lean Playground へジャンプするボタン が現れるようになっています. またコードブロックの中には，import 文が足りないなどの理由でそのままでは実行できないものがありますが，そうした場合は画面右上の実行ボタン をクリックしていただければ，ファイル全体を実行することができます．

スポンサー

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

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