Lean
https://gyazo.com/226a3128deb888a6c8fe053ecacbaccc
https://lean-lang.org/
純粋関数型プログラミング言語 であるとともに 定理証明支援系 でもある
Playground: https://live.lean-lang.org/
環境構築: https://lean-lang.org/documentation/setup/
VSCode の拡張を入れたら必要なものはインストールされるっぽい？
https://marketplace.cursorapi.com/items?itemName=leanprover.lean4
IDE に依存させるのはなんか気持ち悪いので手動で入れる
バージョンアップツールである elan を先に入れる
$ curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
パッケージ管理ツールである lake もこれに付随する
elan 自体のアップデート
$ elan self update
パスを通す
code:.zshrc
export PATH=$PATH:$HOME/.elan/bin
最新バージョンの Lean をインストール + 有効化
$ elan default leanprover/lean4:stable
チュートリアル
言語
https://lean-lang.org/functional_programming_in_lean/
定理証明
https://adam.math.hhu.de
https://leanprover-community.github.io/mathematics_in_lean/index.html
https://lean-lang.org/theorem_proving_in_lean4/
パッケージレジストリ
https://reservoir.lean-lang.org/
#プログラミング言語 #定理証明