lean_workbook_plus_55368

Proved

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

Solve in $Z$ the system equation: $|x-2015|+y^2-3z=4$ , $|y-2015|+z^2-3x=4$ , $|z-2015|+x^2-3y=4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55368 (x y z: ℤ) (h1 : |x - 2015| + y ^ 2 - 3 * z = 4) (h2 : |y - 2015| + z ^ 2 - 3 * x = 4) (h3 : |z - 2015| + x ^ 2 - 3 * y = 4) : x = 2015 ∧ y = 2015 ∧ z = 2015   :=  by sorry

Source

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

View graph