lean_workbook_plus_80259

Proved

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

Prove that if $a, b, c>0$ , then \n $\frac{1}{2}\left ( a^{2}+b^{2}+c^{2}+\frac{9abc}{a+b+c}-2ab-2bc-2ca \right )+\frac{7}{4}\left ( \left ( a-b \right )^{2}+\left ( b-c \right ) ^{2}+\left ( c-a \right )^{2}\right )\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80259 {a b c : ℝ} (ha : a > 0) (hb : b > 0) (hc : c > 0) : (1 / 2) * (a ^ 2 + b ^ 2 + c ^ 2 + (9 * a * b * c) / (a + b + c) - 2 * a * b - 2 * b * c - 2 * c * a) + (7 / 4) * ((a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2) ≥ 0   :=  by sorry

Source

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

View graph