また、
Leanは、数学の形式化や形式検証のために開発された関数型プログラミング言語および定理証明器です(>>767)