lean_workbook_plus_5709

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Or equivalently $(16x + 56)(2x^2 + 14x + 56) = 4y^3$ which may be written as $(2x + 7)^3 + 63(2x + 7) = y^3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5709 (x y : ℤ) : (16*x + 56)*(2*x^2 + 14*x + 56) = 4*y^3 ↔ (2*x + 7)^3 + 63*(2*x + 7) = y^3   :=  by sorry

Source