lean_workbook_plus_82095

Disproved

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

proofwiki

For $k> 3$ , prove that the equation $x^2+y^2+z^2 = kxyz$ doesn't have any integer solutions.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_82095 (k : ℤ) (h : k > 3) : ¬ (∃ x y z : ℤ, x^2 + y^2 + z^2 = k * x * y * z)   :=  by sorry

Source