Lean (証明アシスタント)

Lean（リーン）は、定理証明支援系、および関数型プログラミング言語である。数学の定理やプログラムの性質や仕様を形式的に記述し、それらについての証明をコンピュータで検査するために用いられる。