generated at
Isabelle

高階論理に基づく汎用定理証明系言語
自動証明能力が高い
ホーア論理のためのライブラリがある
HOLの後続システム

website
github
Scala実装, Standard ML実装


入門記事
https://qiita.com/myuon_myon/items/11bb5bfc2e274fdaea7c


プログラムを書いて apply(vcg) を実行すると論理式に変換される
これは人間にも読めるので、数式で見ることでデバッグができる

>数学的な記述をそっくりそのままの形で形式検証できるようにしようという Isabelle の野心的な挑戦が数学界隈で全然知られていないのが悲しすぎる ref

型クラス
https://caeruiro.hatenadiary.org/entry/20100516/1274018433

事例
ケプラー予想
中心極限定理
https://link.springer.com/article/10.1007/s10817-017-9404-x?wt_mc=alerts.TOCjournals


https://blog.kuniwak.com/entry/2020/12/19/111404
https://m-hiyama.hatenablog.com/entry/20160609/1465433202
https://swet.dena.com/entry/2022/08/04/181425
OCamlから変換できるんだ
Isar
https://isabelle.in.tum.de/doc/tutorial.pdf

#プログラミング言語