Lean4について調べた

n月刊ラムダノート Vol.5, No.1(2025)でLean言語(Lean4)について知ったので自分用インデックスとして参考文献を貼っていく
https://www.lambdanote.com/products/n-vol-5-no-1

日本語化されているドキュメント
https://zenn.dev/leanja/articles/lean_ja_2024_work

Lean4のインストール
https://aconite-ac.github.io/how_to_install_lean/title_page.html

macOSはこれだけ

$ brew install elan-init
$ elan toolchain install stable

VSCode拡張
https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

AWSが開発する認可フレームワークのCedarは開発にLeanを取り入れている
https://www.cedarpolicy.com/en

解説ブログ
LeanとRustの実装に同じ入力を与えて検証している
https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/

コード
https://github.com/cedar-policy/cedar-spec/tree/main/cedar-lean

CedarはAmazon Verified PermissionsとしてManaged serviceが提供されている
https://aws.amazon.com/verified-permissions/

PHPerKaigi 2025でCedarについて発表がある予定
https://fortee.jp/phperkaigi-2025/proposal/f1d9f83e-790a-41be-a0e9-3a8a47cc164f

同じ人が関数型まつりでLeanにも触れるCfPを出している
日の目を見てほしい
https://fortee.jp/2025fp-matsuri/proposal/8bb407b5-5df3-48bb-a934-0ca6ca628c9a

AWSの中の人によるCedarの動画
https://www.youtube.com/watch?v=KC6rlcsHUVs

Leanprover Communityによる年次イベントLean Togetherの動画が上がっている
https://www.youtube.com/@leanprovercommunity5485/videos

Lean Together含む過去のイベントとこれからのイベント一覧
https://leanprover-community.github.io/events.html