Prove2Me

lean_workbook_plus_9051

Proved

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

For a,b,ca, b, c non-negative numbers prove that:\n\n (a2+ab+b2)(b2+bc+c2)(c2+ca+a2)≥\n\n13⋅(ab+bc+ca)2⋅(a+b+c)2  ;(a^2+ab+b^2)(b^2+bc+c^2)(c^2+ca+a^2) \ge \n\n \frac{1}{3} \cdot (ab+bc+ca)^2 \cdot (a+b+c)^2 \ \ ;\n\nGreetings!

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

View graph