lean_workbook_plus_66088

Proved

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

Let $y = x-1$ . We have that\n\n $x^4 + (x-2)^4 = (y+1)^4 + (y-1)^4 = 2y^4 + 12y^2 + 2 = 34 \Rightarrow y^4 + 6y^2 - 16 = 0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_66088  (x y : ℝ)
  (h₀ : y = x - 1)
  (h₁ : x^4 + (x - 2)^4 = 34) :
  y^4 + 6 * y^2 - 16 = 0   :=  by sorry

Source