LEAN

定理証明支援系 LEAN に関する情報整理。

LEANとは

Microsoft Reserachが中心になり開発している定理証明支援系。
LENAの証明言語の文法に従い定理等の証明を記述すると
その証明が形式論理的に正しいか否か LEANがチェックする。

◇LEAN公式サイト ⇒　こちら

◇インストール方法　⇒　こちら