lean_workbook_plus_36877

Proved

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

Setting $x = {a^2} + {b^2} + {c^2};y = ab + bc + ca$ and rewrite the inequality as the form of $x,y$ . We need to prove $\frac{{3x}}{{4\left( {x + 2y} \right)}} + \frac{3}{4} \le \frac{{2x + 4y}}{{x + 5y}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36877 {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hxy : x + y = 1) : 3 * x / (4 * (x + 2 * y)) + 3 / 4 ≤ 2 * x + 4 * y / (x + 5 * y)   :=  by sorry

Source

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

View graph