lean_workbook_plus_37502

Proved

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

Let $y=2z$ , thus we have: $(x+2)^{4}-x^{4}=y^{3}\iff x^{3}+3x^{2}+4x+2=z^{3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37502 (x y z: ℤ) (h₁ : y = 2 * z) : (x + 2) ^ 4 - x ^ 4 = y ^ 3 ↔ x ^ 3 + 3 * x ^ 2 + 4 * x + 2 = z ^ 3   :=  by sorry

Source