01 / UNDERSTAND
仕組みと使いどころ
定理証明支援系（Proof Assistant）は、定義や命題、証明を厳密な形式で表し、検証するために使われます。Leanは、形式証明と検証可能なコードを記述できるオープンソースのプログラミング言語兼定理証明支援系です。信頼対象を小さくしたカーネルが証明を確認し、自動化機能はパターン分岐や不等式などの証明作業を支援します。また、独自の記法や証明自動化を拡張できます。ただし、確認の対象は形式化して入力された定義・命題・証明であり、資料はあらゆる命題を自動で証明できるとはしていません。
02 / IN PRACTICE
Proof Assistantの活用例
たとえば、こんな場面で
活用例として、素数の定義と「素数は無限に存在する」という定理をLeanで形式化し、証明の各段階が論理規則に従っているかをカーネルに確認させる方法があります。ソフトウェアやハードウェアの性質を形式化して検証する用途にも利用できます。
03 / GOOD TO KNOW
使うときのポイント
導入時は、何を定義・命題として形式化するのかを明確にし、自動化機能が証明を支援する範囲と、カーネルが最終的に確認する範囲を分けて捉えることが重要です。
参考資料
Lean Programming Language （新しいタブで開きます）用語の説明や活用例に関連する参考資料です。
READ & LEARN
記事一覧を見る 用語を知ったら、活用を知る。
AI LABで、AIの動向や業務に取り入れるヒントを読む。