Prove2Me

lean_workbook_plus_82179

Proved

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

proofwiki

Prove that if a,b,c>0a,b,c>0 then \n (a2+b2+c2)2+(ab+bc+ca)2≥2(a2+b2+c2)(ab+bc+ca).(a^2+b^2+c^2)^2+(ab+bc+ca)^2\geq 2(a^2+b^2+c^2)(ab+bc+ca).\n

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

View graph