For every non-negative integer n, the expression n^4 + n^2 is divisible by 2.

Enuntiatio — the claim

For every non-negative integer n, the expression n^4 + n^2 is divisible by 2.

Refuted by Some non-negative integer n makes n^4 + n^2 leave a nonzero remainder modulo 2.

Expressio — the formal statement

import Mathlib

theorem n4_add_n2_div_two (n : Nat) : (n^4 + n^2) % 2 = 0

Demonstratio — the kernel-checked proof

by
  induction n with
  | zero => rfl
  | succ k ih =>
    rcases Nat.even_or_odd k with ⟨m, hm⟩ | ⟨m, hm⟩
    · subst hm
      ring_nf
      omega
    · subst hm
      ring_nf
      omega