Lean-Workbook Syntax 70836: A fourth-power bound for a sum of cubes

Proved

WorkbookSyntax.plus_70836

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

For every natural $n$ , $\sum_{i=0}^{n}i^3\le n^4$ .

Source: Lean-Workbook row lean_workbook_plus_70836 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble

import Mathlib.Algebra.BigOperators.Intervals

Formal statement

theorem WorkbookSyntax.plus_70836 (n : ℕ) : ∑ i ∈ Finset.range (n+1), i^3 ≤ n^4   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_70836; immutable original Prove2Me node 05b6dea1-9caf-4bab-8c5a-f5f8da278995

View graph