lean_workbook_plus_34923

Disproved

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

Let $x,y,z$ be positive real numbers , prove that : \n $A = \frac{1}{2(y^2+z^2+yz)} + \frac{1}{2(y^2+x^2+yx)} + \frac{z}{2(x^2+xy+y^2)} + \frac{x+y+z}{3} \geq \frac{3}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34923 : ∀ x y z : ℝ, (x > 0 ∧ y > 0 ∧ z > 0 →  1 / (2 * (y ^ 2 + z ^ 2 + y * z)) + 1 / (2 * (y ^ 2 + x ^ 2 + y * x)) + z / (2 * (x ^ 2 + y * x + y ^ 2)) + (x + y + z) / 3 >= 3 / 2 )   :=  by sorry

Source

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

View graph