Prove2Me

lean_workbook_plus_49924

Disproved

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

prove that: G.1−(3 x+y)(3 z+y)2 (3 x+y)(3 z+y)+(3 x+z)(3 y+z)−(3 x+z)(3 y+z)2 (3 x+z)(3 y+z)+(3 y+x)(3 z+x)−(3 y+x)(3 z+x)2 (3 y+x)(3 z+x)+(3 x+y)(3 z+y)≥0G.1-{\frac { \left( 3\,x+y \right) \left( 3\,z+y \right) }{2\, \left( 3\,x+y \right) \left( 3\,z+y \right) + \left( 3\,x+z \right) \left( 3\,y+z \right) }}-{\frac { \left( 3\,x+z \right) \left( 3\,y+z \right) }{2\, \left( 3\,x+z \right) \left( 3\,y+z \right) + \left( 3\,y+x \right) \left( 3\,z+x \right) }}-{\frac { \left( 3\,y+x \right) \left( 3\,z+x \right) }{2\, \left( 3\,y+x \right) \left( 3\,z+x \right) + \left( 3\,x+y \right) \left( 3\,z+y \right) }}\geq 0

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

View graph