Prove2Me

lean_workbook_plus_59946

Proved

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

By Cauchy-Schwarz: \n (ab+c)2+(bc+a)2+(ca+b)2≥13.(ab+c+bc+a+ca+b)2(\frac{a}{b+c})^2+(\frac{b}{c+a})^2+(\frac{c}{a+b})^2\ge{\frac{1}{3}.(\frac{a}{b+c}+\frac{b}{c+a}+\frac{c}{a+b})^2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59946 : ∀ a b c : ℝ, (a / (b + c)) ^ 2 + (b / (c + a)) ^ 2 + (c / (a + b)) ^ 2 ≥ 1 / 3 * (a / (b + c) + b / (c + a) + c / (a + b)) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph