lean_workbook_plus_34683Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)prove that: 2 xy+2 xz+2 yz≤(z+xy)(x+yz)z+x+(y+xz)(x+yz)x+y+(z+xy)(y+xz)y+z2\,xy+2\,xz+2\,yz\le {\frac { \left( z+xy \right) \left( x+yz \right) }{z+x}}+{\frac { \left( y+xz \right) \left( x+yz \right) }{x+y}}+{\frac { \left( z+xy \right) \left( y+xz \right) }{y+z}}2xy+2xz+2yz≤z+x(z+xy)(x+yz)+x+y(y+xz)(x+yz)+y+z(z+xy)(y+xz)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_34683 : ∀ x y z : ℝ, 2 * x * y + 2 * x * z + 2 * y * z ≤ (z + x * y) * (x + y * z) / (z + x) + (y + x * z) * (x + y * z) / (x + y) + (z + x * y) * (y + x * z) / (y + z) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph