lean_workbook_plus_48285

Disproved

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

prove that: ${\frac {xy}{ \left( 1+z \right) \left( y+z \right) \left( z+x \right) }}+{\frac {yz}{ \left( 1+x \right) \left( x+y \right) \left( z+x \right) }}+{\frac {xz}{ \left( 1+y \right) \left( x+y \right) \left( y+z \right) }}\leq \frac{1}{72}(x+y+z)^3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48285 : ∀ x y z : ℝ, (x * y / (1 + z) / (y + z) / (z + x) + y * z / (1 + x) / (x + y) / (z + x) + x * z / (1 + y) / (x + y) / (y + z)) ≤ 1 / 72 * (x + y + z) ^ 3   :=  by sorry

Source

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

View graph