For every non-negative integer n, the expression n^4 + n^3 + n^2 + n + 1 is never divisible by 4; its residue modulo 4 always lies in {1, 2, 3}.

Enuntiatio — the claim

For every non-negative integer n, the expression n^4 + n^3 + n^2 + n + 1 is never divisible by 4; its residue modulo 4 always lies in {1, 2, 3}.

Refuted by Some non-negative integer n makes n^4 + n^3 + n^2 + n + 1 divisible by 4, i.e. (n^4+n^3+n^2+n+1) % 4 == 0.

Expressio — the formal statement

import Mathlib

theorem poly_never_div_four (n : ℕ) : (n^4 + n^3 + n^2 + n + 1) % 4 ≠ 0

Demonstratio — the kernel-checked proof

by
  have aux (r : ℕ) (h : r < 4) : (r^4 + r^3 + r^2 + r + 1) % 4 ≠ 0 := by
    have h_cases : r = 0 ∨ r = 1 ∨ r = 2 ∨ r = 3 := by
      have : r ≤ 3 := by omega
      omega
    rcases h_cases with (hr|hr|hr|hr)
    · subst hr; decide
    · subst hr; decide
    · subst hr; decide
    · subst hr; decide
  have h_mod := Nat.mod_add_div n 4
  have h_lt : n % 4 < 4 := Nat.mod_lt n (by norm_num)
  have h_residue := aux (n % 4) h_lt
  have h_mod_eq : (n^4 + n^3 + n^2 + n + 1) % 4 = ((n % 4)^4 + (n % 4)^3 + (n % 4)^2 + (n % 4) + 1) % 4 := by
    have h_pow_mod (k : ℕ) : n^k % 4 = (n % 4)^k % 4 := by
      simpa [Nat.pow_mod] using rfl
    calc
      (n^4 + n^3 + n^2 + n + 1) % 4 = ((n^4) % 4 + (n^3) % 4 + (n^2) % 4 + n % 4 + 1 % 4) % 4 := by
        simp [Nat.add_mod]
      _ = (((n % 4)^4 % 4) + ((n % 4)^3 % 4) + ((n % 4)^2 % 4) + (n % 4) + 1 % 4) % 4 := by
        simp [h_pow_mod 4, h_pow_mod 3, h_pow_mod 2]
      _ = (((n % 4)^4) + ((n % 4)^3) + ((n % 4)^2) + (n % 4) + 1) % 4 := by
        simp [Nat.add_mod]
      _ = ((n % 4)^4 + (n % 4)^3 + (n % 4)^2 + (n % 4) + 1) % 4 := rfl
  rw [h_mod_eq]
  exact h_residue