01 / UNDERSTAND
仕組みと使いどころ
Leanでは、数学の概念を厳密に定義し、命題とその形式的な証明を記述できます。小さな信頼済みカーネルが証明を検査するため、数学的証明の確認や、ソフトウェア・ハードウェアに求める性質の形式検証に利用できます。組み込みの証明支援機能に加え、メタプログラミングによって独自の記法や証明自動化を拡張できます。ただし、Leanが確認するのはLean上で明確に記述された定義・命題・証明です。対象を正確に形式化し、必要な証明を用意する作業そのものが不要になるわけではありません。
02 / IN PRACTICE
Leanの活用例
たとえば、こんな場面で
例えば、素数をLeanで定義し、「任意の1より大きい自然数には素因数が存在する」といった命題を記述して証明を検査できます。また、プログラムに期待する性質を命題として表し、その性質が成り立つことを形式的に確認する用途も考えられます。
03 / GOOD TO KNOW
使うときのポイント
利用時は、検証したい性質が定義や命題に正確に反映されているかを確認します。自動化機能は証明を支援しますが、形式化する内容の適切さまで自動で保証するものではありません。
参考資料
Lean Programming Language （新しいタブで開きます）用語の説明や活用例に関連する参考資料です。
READ & LEARN
記事一覧を見る 用語を知ったら、活用を知る。
AI LABで、AIの動向や業務に取り入れるヒントを読む。