Prove2Me

lean_workbook_plus_48606

Disproved

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

      p2+5r2≥16Rr⇔(x+y+z)2+5xyzx+y+z≥16xyzx+y+z.(x+y)(y+z)(z+x)4xyz(x+y+z)⇔(x+y+z)2+5xyzx+y+z≥4(x+y)(y+z)(z+x)(x+y+z)⇔(x+y+z)3+5xyz≥4(x+y)(y+z)(z+x)⇔x3+y3+z3+3xyz≥xy(x+y)+yz(y+z)+zx(z+x)\begin{array}{l} \,\,\,\,\,\,{p^2} + 5{r^2} \ge 16Rr\\ \Leftrightarrow {\left( {x + y + z} \right)^2} + \frac{{5xyz}}{{x + y + z}} \ge 16\sqrt {\frac{{xyz}}{{x + y + z}}} .\frac{{\left( {x + y} \right)\left( {y + z} \right)\left( {z + x} \right)}}{{4\sqrt {xyz\left( {x + y + z} \right)} }}\\ \Leftrightarrow {\left( {x + y + z} \right)^2} + \frac{{5xyz}}{{x + y + z}} \ge 4\frac{{\left( {x + y} \right)\left( {y + z} \right)\left( {z + x} \right)}}{{\left( {x + y + z} \right)}}\\ \Leftrightarrow {\left( {x + y + z} \right)^3} + 5xyz \ge 4\left( {x + y} \right)\left( {y + z} \right)\left( {z + x} \right)\\ \Leftrightarrow {x^3} + {y^3} + {z^3} + 3xyz \ge xy\left( {x + y} \right) + yz\left( {y + z} \right) + zx\left( {z + x} \right) \end{array}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48606 : ∀ x y z : ℝ, (x + y + z)^3 + 5 * x * y * z ≥ 4 * (x + y) * (y + z) * (z + x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph