Prove2Me

lean_workbook_plus_35900

Proved

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

Note that (a+b+c)2−32(a(b+c)+b(c+a)+c(a+b))=∑12(a−b)2≥0 (∗) (a+b+c)^2-\frac{3}{2}(a(b+c)+b(c+a)+c(a+b)) = \sum \frac{1}{2}(a-b)^2 \geq 0 \ (*) , whence it follows that \n\n ∑ab+c=∑a2a(b+c)≥(a+b+c)2a(b+c)+b(c+a)+c(a+b)≥32 \sum \frac{a}{b+c} = \sum \frac{a^2}{a(b+c)} \geq \frac{(a+b+c)^2}{a(b+c)+b(c+a)+c(a+b)} \geq \frac{3}{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35900  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) :
  a / (b + c) + b / (c + a) + c / (a + b) ≥ 3 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph