lean_workbook_plus_78942

Disproved

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

prove that ${\frac {{x}^{2}+{y}^{2}}{x+y}}+{\frac {{y}^{2}+{z}^{2}}{y+z}}+{\frac {{x}^{2}+{z}^{2}}{z+x}}\geq {\frac {9}{8}}\,{\frac {\sqrt {3}\sqrt {{x}^{2}+{y}^{2}+{z}^{2}} \left( y+z \right) \left( z+x \right) \left( x+y \right) }{ \left( x+y+z \right) \left( xy+xz+yz \right) }}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78942 : ∀ x y z : ℝ, (x + y + z ≠ 0 ∧ x * y + x * z + y * z ≠ 0 → x^2 + y^2 + z^2 ≠ 0 → (x^2 + y^2) / (x + y) + (y^2 + z^2) / (y + z) + (z^2 + x^2) / (z + x) ≥ (9 / 8) * Real.sqrt 3 * Real.sqrt (x^2 + y^2 + z^2) * (y + z) * (z + x) * (x + y) / ((x + y + z) * (x * y + x * z + y * z)))   :=  by sorry

Source

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

View graph