lean_workbook_plus_34258

Proved

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

Solve the system equations\n\n $x^{4}-y^{4}=240\nx^{3}-2y^{3}=3(x^{2}-4y^{2})-4(x-8y)$ \nIt gives $(x-2)^4=(y-4)^4$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34258 (x y : ℝ) (h₁ : x^4 - y^4 = 240) (h₂ : x^3 - 2*y^3 = 3*(x^2 - 4*y^2) - 4*(x - 8*y)) : (x - 2)^4 = (y - 4)^4   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph