Lean-Workbook Syntax 61272: The sum of the first twenty cubes

$1^3+2^3+\cdots+20^3=44100$.

Source: Lean-Workbook row lean_workbook_plus_61272 (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.