計算機援用証明

計算機援用証明とは、コンピュータによって少なくとも一部が生成された数学的証明である。今日における計算機援用証明のほとんどは数学的定理に対するしらみつぶし法の実装である。