A fourth-power identity for powers of2002

Proved

WorkbookSource.problem_22683

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

(6·2002^n)^4+(5·2002^n)^4+(3·2002^n)^4=2002^{4n+1} for all $n\in\mathbb{N}$

Source: InternLM Lean-Workbook, record lean_workbook_22683 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_22683 : ∀ n : ℕ, (6 * 2002 ^ n) ^ 4 + (5 * 2002 ^ n) ^ 4 + (3 * 2002 ^ n) ^ 4 = 2002 ^ (4 * n + 1)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_22683; Apache-2.0

View graph