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

Enuntiatio — the claim

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

Refuted by Any non-negative integer n for which (n^2 + n + 1) % 5 equals 0 or 4 would refute the claim.

Expressio — the formal statement

import Mathlib

theorem sq_add_self_add_one_mod_five (n : Nat) : (n^2 + n + 1) % 5 = 1 ∨ (n^2 + n + 1) % 5 = 2 ∨ (n^2 + n + 1) % 5 = 3

Demonstratio — the kernel-checked proof

by
  have h : (n^2 + n + 1) % 5 = 1 ∨ (n^2 + n + 1) % 5 = 2 ∨ (n^2 + n + 1) % 5 = 3 := by
    have h₁ : n % 5 = 0 ∨ n % 5 = 1 ∨ n % 5 = 2 ∨ n % 5 = 3 ∨ n % 5 = 4 := by omega
    rcases h₁ with (h₁ | h₁ | h₁ | h₁ | h₁)
    · -- Case: n ≡ 0 mod 5
      have h₂ : (n^2 + n + 1) % 5 = 1 := by
        have h₃ : n % 5 = 0 := h₁
        have h₄ : (n^2 + n + 1) % 5 = 1 := by
          have h₅ : n % 5 = 0 := h₃
          have h₆ : (n^2 + n + 1) % 5 = ( (n % 5)^2 + (n % 5) + 1 ) % 5 := by
            simp [Nat.add_mod, Nat.pow_mod, Nat.mul_mod]
          rw [h₆]
          simp [h₅]
          <;> norm_num
        exact h₄
      exact Or.inl h₂
    · -- Case: n ≡ 1 mod 5
      have h₂ : (n^2 + n + 1) % 5 = 3 := by
        have h₃ : n % 5 = 1 := h₁
        have h₄ : (n^2 + n + 1) % 5 = 3 := by
          have h₅ : n % 5 = 1 := h₃
          have h₆ : (n^2 + n + 1) % 5 = ( (n % 5)^2 + (n % 5) + 1 ) % 5 := by
            simp [Nat.add_mod, Nat.pow_mod, Nat.mul_mod]
          rw [h₆]
          simp [h₅]
          <;> norm_num
        exact h₄
      exact Or.inr (Or.inr h₂)
    · -- Case: n ≡ 2 mod 5
      have h₂ : (n^2 + n + 1) % 5 = 2 := by
        have h₃ : n % 5 = 2 := h₁
        have h₄ : (n^2 + n + 1) % 5 = 2 := by
          have h₅ : n % 5 = 2 := h₃
          have h₆ : (n^2 + n + 1) % 5 = ( (n % 5)^2 + (n % 5) + 1 ) % 5 := by
            simp [Nat.add_mod, Nat.pow_mod, Nat.mul_mod]
          rw [h₆]
          simp [h₅]
          <;> norm_num
        exact h₄
      exact Or.inr (Or.inl h₂)
    · -- Case: n ≡ 3 mod 5
      have h₂ : (n^2 + n + 1) % 5 = 3 := by
        have h₃ : n % 5 = 3 := h₁
        have h₄ : (n^2 + n + 1) % 5 = 3 := by
          have h₅ : n % 5 = 3 := h₃
          have h₆ : (n^2 + n + 1) % 5 = ( (n % 5)^2 + (n % 5) + 1 ) % 5 := by
            simp [Nat.add_mod, Nat.pow_mod, Nat.mul_mod]
          rw [h₆]
          simp [h₅]
          <;> norm_num
        exact h₄
      exact Or.inr (Or.inr h₂)
    · -- Case: n ≡ 4 mod 5
      have h₂ : (n^2 + n + 1) % 5 = 1 := by
        have h₃ : n % 5 = 4 := h₁
        have h₄ : (n^2 + n + 1) % 5 = 1 := by
          have h₅ : n % 5 = 4 := h₃
          have h₆ : (n^2 + n + 1) % 5 = ( (n % 5)^2 + (n % 5) + 1 ) % 5 := by
            simp [Nat.add_mod, Nat.pow_mod, Nat.mul_mod]
          rw [h₆]
          simp [h₅]
          <;> norm_num
        exact h₄
      exact Or.inl h₂
  exact h