lean_workbook_plus_24205
ProvedProve that implies .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24205 (n : ℕ) : (n * (n + 1) * (2 * n + 1) / 6) ≤ 2003 → n ≤ 17 := by sorry
Source
Prove that implies .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_24205 (n : ℕ) : (n * (n + 1) * (2 * n + 1) / 6) ≤ 2003 → n ≤ 17 := by sorry