Prove2Me

lean_workbook_plus_56175

Proved

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

Solve the Diophantine equation x3y2+y3x2+(xy)2=z3x^{3}y^2+y^{3}x^2+(xy)^2=z^3 for positive integers (x,y)(x,y), where (x,y)>1(x,y)>1 and g.c.d(x,y)=1g.c.d(x,y)=1 for positive integer values of zz.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56175 (x y z : ℕ) (h1 : 1 < x ∧ 1 < y ∧ 1 < z) (h2 : Nat.gcd x y = 1) (h3 : x^3*y^2 + y^3*x^2 + (x*y)^2 = z^3) : ∃ x y z : ℕ, (1 < x ∧ 1 < y ∧ 1 < z ∧ Nat.gcd x y = 1 ∧ x^3*y^2 + y^3*x^2 + (x*y)^2 = z^3)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph