For every non-negative integer n, the expression n^3 + 5*n is divisible by 3.

Enuntiatio — the claim

For every non-negative integer n, the expression n^3 + 5*n is divisible by 3.

Refuted by Some non-negative integer n makes n^3 + 5*n not divisible by 3.

Expressio — the formal statement

import Mathlib

theorem n_cubed_plus_five_n_div_three (n : ℕ) : (n^3 + 5*n) % 3 = 0

Demonstratio — the kernel-checked proof

by
  induction n with
  | zero => rfl
  | succ k ih =>
    have h : (k + 1)^3 + 5*(k+1) = (k^3 + 5*k) + 3*(k^2 + k + 2) := by ring
    rw [h, Nat.add_mul_mod_self_left, ih]