lean_workbook_plus_40055

Proved

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

Let $x=a^2+b^2+c^2$ and $y=ab+bc+ca$ . It is enough to show that \n $6+27-\frac{18(x+2y)}{2x+y} \le \frac{15x}y \iff (x-y)(10x-y) \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40055 {x y : ℝ} (hx : x > 0) (hy : y > 0) (hxy : x + y = 1) : 6 + 27 - (18 * (x + 2 * y)) / (2 * x + y) ≤ 15 * x / y ↔ (x - y) * (10 * x - y) ≥ 0   :=  by sorry

Source

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

View graph