Brief Introduction to Lean Programming Language
https://gyazo.com/c9156e01c5000f81382af1ffdfc72f38
ひきこまりの吸血鬼の悶々
画像が無いのでとりあえずこれで
#スライド
#Lean
自己紹介
https://scrapbox.io/api/pages/sno2wman/sno2wman/icon#.png
SnO2WMaN
論理学とインターネットが大好きということになっている
作ったWebサービス
OTOMADB：音MADのデータベース
はじめに
Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover.
Leanは定理証明支援系 / 関数型プログラミング言語 の両方を持つ言語です．
最近バージョン4(Lean 4)が安定リリースに達しました．
Leanは、 生まれたばかりのプログラミング言語です。 応援して下さいね☆
そもそも定理証明支援系とは
Curry-Howard同型対応などによって「証明 = 計算 = プログラム」のような視座がある．
4色問題など数学の定理の中には証明がありえないほど複雑怪奇で長いものもある．
人間では検証するのがムリなので，計算をミスしない計算機に（プログラムを書くことで）証明をやらせよう
この試みを形式化(Formalized)という．
形式化された証明は（定理証明支援系の実装がおかしくない限りは）厳密かつミスの無い証明になる
よく知られている定理証明支援系
古典的にはCoqやIsabelleなど，
最近ではAgdaやIdris（こちらはプログラミング言語の面も強い）
こういう人にオススメ: ともあれ定理証明支援系に触ってみたい
型のある数式：手書き / TeXの数式には型がない
開発体験の良さ
個人的な体感で，2023年でおそらく最もモダンな定理証明支援系はLeanです．
公式のVSCode拡張機能がかなり充実している
https://gyazo.com/77d417983de5384fe980728ea3a6ad0b
なおInfo ViewはJavaScript / Reactなどで拡張することが出来る
例えばルービックキューブを表示したり…
https://raw.githubusercontent.com/leanprover-community/lean4-samples/main/RubiksCube/images/screenshot.png
https://github.com/leanprover-community/lean4-samples/tree/main/RubiksCube
他との優位性
CoqやIsabelleは専用のエディタを用意しなければならない．一応VSCode拡張機能があるが…
AgdaやIdrisはEmacsの利用者が多い関係かVSCodeの対応があまり微妙
数学ライブラリの充実さ
「○○の定理より～～」とか書くの、人類の叡智から答案にimportしてるような気持になってすごく楽しい@M4ki2ush1
群論や環論，集合論や数論などの基本的な数学的事実はコミュニティによってMathlib4というリポジトリで予め証明されている
https://leanprover-community.github.io/mathlib4_docs/
その他の話題
最近，Telence Taoが自身の理論をLeanで形式化することでミスを発見している
https://mathstodon.xyz/@tao/111287749336059662
https://twitter.com/henomoto1025/status/1717059218820468856
大規模言語モデルと接続させて，AIに証明を支援させたり，自動で証明してくれるようにしようと模索され始めている
LeanDojo
https://leandojo.org/
https://arxiv.org/abs/2306.15626
https://morph.so/blog/the-personal-ai-proof-engineer/
こういう人にオススメ: 関数型プログラミング言語の入門
Lean 4は関数型プログラミング言語としても使うことが出来る
拡張のない純粋なHaskellと比較して大きく異なるのは，Leanには依存型がある
依存型とは項に依存した型．
例えば「長さが5のリスト」とか「24以下の自然数」みたいなより強い型付けが行える．
確かMartin-Löf型理論ベースだった記憶がある
更に定理証明支援系としての特色を活かして，定義した関数が何らかの性質を満たすことを証明したりすることでバグがないことを保証したりできる．
とはいっても現状ではまだまだ全然ライブラリは無いので，実用的なアプリケーションが作れるかはさておき…
せいぜいCLIツールを書くぐらいだろうか？
現状では標準でネットワーク通信すら用意されていない
私的な話
私は論理学（主に様相論理関連）の諸々の成果をLean 4で形式化したいと試みている．
最近はFormalizedFormalLogic/FoundationによってLean 4でGödelの第1不完全性定理が証明された
参考文献
短い時間の発表なので，いくつか参考文献をまとめておく．
注意：Lean 3とLean 4があり，3系と4系にはほとんど互換性がないので文献には注意すること．
https://lean-lang.org/lean4/doc/quickstart.html
Leanそのもののドキュメント
インストール方法など
https://lean-lang.org/lean4/doc/quickstart.html
https://lean-lang.org/functional_programming_in_lean
LeanをHaskellのような関数型プログラミング言語として入門する際の公式ガイド．
https://lean-lang.org/theorem_proving_in_lean4/
Leanを普通に定理証明支援系として使う際の公式ガイド．
関数型言語”兼”定理証明支援系Leanの環境構築
ここの参考文献も参照せよ
lean-ja：Leanの日本語コミュニティ
https://github.com/lean-ja
いくつかの非公式な日本語訳が行われている
Mathematics in type thoery 日本語訳
https://lean-ja.github.io/tactic-cheatsheet/
タクティクのチートシート