Brief Introduction to Lean Programming Language
https://gyazo.com/c9156e01c5000f81382af1ffdfc72f38
画像が無いのでとりあえずこれで
自己紹介
https://scrapbox.io/api/pages/sno2wman/sno2wman/icon#.png
作ったWebサービス
はじめに
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.
最近バージョン4(Lean 4)が安定リリースに達しました. Leanは、 生まれたばかりのプログラミング言語です。 応援して下さいね☆
4色問題など数学の定理の中には証明がありえないほど複雑怪奇で長いものもある. 人間では検証するのがムリなので,計算をミスしない計算機に(プログラムを書くことで)証明をやらせよう
この試みを形式化(Formalized)という.
形式化された証明は(定理証明支援系の実装がおかしくない限りは)厳密かつミスの無い証明になる
よく知られている定理証明支援系
開発体験の良さ
https://gyazo.com/77d417983de5384fe980728ea3a6ad0b
https://raw.githubusercontent.com/leanprover-community/lean4-samples/main/RubiksCube/images/screenshot.png
他との優位性
数学ライブラリの充実さ
「○○の定理より~~」とか書くの、人類の叡智から答案にimportしてるような気持になってすごく楽しい@M4ki2ush1 その他の話題
大規模言語モデルと接続させて,AIに証明を支援させたり,自動で証明してくれるようにしようと模索され始めている 例えば「長さが5のリスト」とか「24以下の自然数」みたいなより強い型付けが行える.
更に定理証明支援系としての特色を活かして,定義した関数が何らかの性質を満たすことを証明したりすることでバグがないことを保証したりできる. とはいっても現状ではまだまだ全然ライブラリは無いので,実用的なアプリケーションが作れるかはさておき…
現状では標準でネットワーク通信すら用意されていない
私的な話
参考文献
短い時間の発表なので,いくつか参考文献をまとめておく.
インストール方法など
Leanを普通に定理証明支援系として使う際の公式ガイド. ここの参考文献も参照せよ
いくつかの非公式な日本語訳が行われている
タクティクのチートシート