lean_workbook_plus_3709

Proved

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

Let a,b,c>0. Prove that \n $3( a^{2} +b^{2} +c^{2})( a^{2}b^{2} +b^{2}c^{2}+c^{2}a^{2})\geq ( a^{2} + ab+b^{2})(b^{2}+bc +c^{2}) ( a^{2} + ac+c^{2})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3709 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : 3 * (a^2 + b^2 + c^2) * (a^2 * b^2 + b^2 * c^2 + c^2 * a^2) ≥ (a^2 + a * b + b^2) * (b^2 + b * c + c^2) * (a^2 + a * c + c^2)   :=  by sorry

Source

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

View graph