Prove2Me

lean_workbook_plus_7539

Proved

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

Find integer solutions x,y,zx, y, z such that xyz≠0xyz \neq 0 and x4+2y4=z2x^4 + 2y^4 = z^2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7539 (x y z : ℤ) (h : x * y * z ≠ 0) : x^4 + 2*y^4 = z^2 ↔ ∃ x0 y0 z0 : ℤ, x0 * y0 * z0 ≠ 0 ∧ x^4 + 2*y^4 = z^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph