lean_workbook_plus_45521

Proved

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

Find all triplets of integers $(x,y,z)$ such that $xy(x^2-y^2)+yz(y^2-z^2)+zx(z^2-x^2)=1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45521 (x y z : ℤ) (h : x * y * (x ^ 2 - y ^ 2) + y * z * (y ^ 2 - z ^ 2) + z * x * (z ^ 2 - x ^ 2) = 1) : (x = 0 ∧ y = 1 ∧ z = 0) ∨ (x = 0 ∧ y = -1 ∧ z = 0) ∨ (x = 1 ∧ y = 0 ∧ z = 0) ∨ (x = -1 ∧ y = 0 ∧ z = 0) ∨ (x = 1 ∧ y = -1 ∧ z = 0) ∨ (x = -1 ∧ y = 1 ∧ z = 0) ∨ (x = 0 ∧ y = 0 ∧ z = 1) ∨ (x = 0 ∧ y = 0 ∧ z = -1) ∨ (x = 1 ∧ y = 0 ∧ z = 1) ∨ (x = -1 ∧ y = 0 ∧ z = -1) ∨ (x = 0 ∧ y = 1 ∧ z = 1) ∨ (x = 0 ∧ y = -1 ∧ z = -1)   :=  by sorry

Source

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

View graph