For every non-negative integer n, the expression (2n)^4 + 2*(2n)^3 + 4*(2n)^2 + 8*(2n) is divisible by 16.

Enuntiatio — the claim

For every non-negative integer n, the expression (2n)^4 + 2*(2n)^3 + 4*(2n)^2 + 8*(2n) is divisible by 16.

Refuted by Some non-negative integer n makes ((2n)^4 + 2*(2n)^3 + 4*(2n)^2 + 8*(2n)) % 16 nonzero.

Expressio — the formal statement

import Mathlib

theorem div16 (n : Nat) : ((2*n)^4 + 2*(2*n)^3 + 4*(2*n)^2 + 8*(2*n)) % 16 = 0

Demonstratio — the kernel-checked proof

by ring_nf; omega