Lean - mrsekut-p

Lean

https://gyazo.com/3fb782c376a2b264dd36e7087b76be06

MicroSoft製の定理証明系言語

Leonardo de Moura

2013〜

Lean 4は2021~

VSCode拡張

日本語コミュニティがある

LEAN勉強会

https://discord.gg/zXT8jyHb

Lean4 タクティク逆引きリスト

https://lean-ja.github.io/tactic-cheatsheet/index.html

lean-jaが管理している

Leanの環境構築

学ぶ用

Theorem Proving in Lean 4

https://aconite-ac.github.io/theorem_proving_in_lean4_ja/title_page.html

数学系のためのLean勉強会

https://github.com/yuma-mizuno/lean-math-workshop

lean-jaのワークショップ？

https://leanprover-community.github.io/index.html

これはなんだ

https://leanprover.github.io/functional_programming_in_lean/

普通にプログラミング言語としての使い方が書いてある

言語の概観やHello World、モナドトランスフォーマー、依存型を使ったプログラミング、パフォーマンスに関する話など ref

https://leanprover-community.github.io/mathematics_in_lean/index.html

普通の数学を対象に、Leanで定理証明をする資料

最近lean3からlean4への対応が完了しており、Theorem Proving in Lean 4よりも分量があるref

Metaprogramming in Lean 4

https://maxima.hatenablog.jp/entry/2020/11/07/002303

https://zenn.dev/labbase/articles/b24dca38e0420d

https://speakerdeck.com/soukouki/slide-6fa2339e-0b42-4f2c-8cfc-422f74e94b27?slide=6

簡単なスライド

https://haruhisa-enomoto.github.io/lean-math-workshop/#スライド

依存型

https://myuon-myon.hatenablog.com/entry/2016/01/09/212750

#プログラミング言語