Prove2Me

lean_workbook_plus_79869

Disproved

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

Subtracting equations 2nd2nd from 1st1st , 3rd3rd from 2nd2nd , 1st1st from 3rd3rd we get:\n\n(x−y)(x+y−2z+5)=0\n(y−z)(y+z−2x+5)=0\n(z−x)(z+x−2y+5)=0(x-y)(x+y-2z+5)=0\n(y-z)(y+z-2x+5)=0\n(z-x)(z+x-2y+5)=0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79869 : ∀ x y z : ℝ, (x - y) * (x + y - 2 * z + 5) = 0 ∧ (y - z) * (y + z - 2 * x + 5) = 0 ∧ (z - x) * (z + x - 2 * y + 5) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph