For every non-negative integer n, the expression n^4 + 4*n^3 + 5*n^2 + 2*n + 8 leaves remainder 8 when divided by 12; equivalently it is divisible by 12 only after subtracting 8, since n^4+4n^3+5n^2+2n = n(n+1)^2(n+2) is divisible by 12.

Enuntiatio — the claim

For every non-negative integer n, the expression n^4 + 4*n^3 + 5*n^2 + 2*n + 8 leaves remainder 8 when divided by 12; equivalently it is divisible by 12 only after subtracting 8, since n^4+4n^3+5n^2+2n = n(n+1)^2(n+2) is divisible by 12.

Refuted by Some n >= 0 makes (n^4 + 4*n^3 + 5*n^2 + 2*n) % 12 nonzero, i.e. n*(n+1)^2*(n+2) not divisible by 12.

Expressio — the formal statement

import Mathlib

theorem poly_mod_twelve (n : ℕ) : (n^4 + 4*n^3 + 5*n^2 + 2*n + 8) % 12 = 8

Demonstratio — the kernel-checked proof

by
  conv_lhs => rw [show n = 12 * (n / 12) + n % 12 from (Nat.div_add_mod n 12).symm]
  generalize hr : n % 12 = r
  have hr12 : r < 12 := by rw [← hr]; exact Nat.mod_lt _ (by norm_num)
  generalize n / 12 = q
  interval_cases r <;> ring_nf <;> omega