Lean
依存型理論
をベースにした定理証明支援系言語
$ {}^{(1)}
Calculus of Inductive Constructions(CIC)
構文はCoq + Haskell風味
Lean 3系とLean 4系に分かれた
Lean 3
系
Lean 3系はメンテナンスフェーズ
Lean 4系
Lean 4
elan
というパッケージマネージャーを使う
Twitter:
Lean（@leanprover）さん / Twitter
Zulip:
Recent conversations - Lean - Zulip
Natural number game
Leanでブロックチェーンを形式検証する
確認用
Q. Lean
参考
(1)
Lean in nLab
Natural Number Game = Lean による定理証明支援を学ぶ - Maxima で綴る数学の旅
プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog)
#形式手法
#定理証明支援系