A sequence characterized by its partial sums of cubes
ProvedWorkbookCorrected.plus_45064corrected-formalizationlean-workbooksequencessource-checked
Let a₁,a₂,… be positive real numbers. Suppose that for every positive integer n, a₁³+⋯+aₙ³ = (a₁+⋯+aₙ)². Then aₙ=n for every positive integer n.
Formalization Note: Restores the source’s positive indices in both partial sums and the conclusion; the original zero-index sums were inconsistent with its claimed formula.
Source: InternLM Lean-Workbook, record lean_workbook_plus_45064 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_45064 (a : ℕ → ℝ) (ha : ∀ n : ℕ, 1 ≤ n → 0 < a n)
(h : ∀ n : ℕ, 1 ≤ n → (∑ i ∈ Finset.range n, (a (i+1))^3)=(∑ i ∈ Finset.range n, a (i+1))^2) :
∀ n : ℕ, 1 ≤ n → a n=(n:ℝ) := by sorrySource