lean_workbook_plus_6476

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find the smallest positive integer $n$ such that $2014^{n} - n^{2014}$ is divisible by $11$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6476 (n : ℕ) : (2014^n - n^2014 ≡ 0 [ZMOD 11]) → n >= 1   :=  by sorry

Source