lean_workbook_plus_37737

Proved

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

For all reals $a$ , $b$ and $c$ prove that: \n $4(a^{2}+ab+b^{2})(b^{2}+bc+c^{2})(c^{2}+ca+a^{2})\ge3(a^2b+a^2c+b^2a+b^2c+c^2a+c^2b)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37737 (a b c : ℝ) : 4 * (a ^ 2 + a * b + b ^ 2) * (b ^ 2 + b * c + c ^ 2) * (c ^ 2 + c * a + a ^ 2) ≥ 3 * (a ^ 2 * b + a ^ 2 * c + b ^ 2 * a + b ^ 2 * c + c ^ 2 * a + c ^ 2 * b) ^ 2   :=  by sorry

Source

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

View graph