Prove2Me

lean_workbook_plus_30544

Proved

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

Prove that if a,b,c≥0a,b,c\geq0 then 3(a2b+b2c+c2a)(ab2+bc2+ca2)≤(a2+b2+c2)33(a^2b+b^2c+c^2a)(ab^2+bc^2+ca^2)\leq(a^2+b^2+c^2)^3.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30544 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : 3 * (a ^ 2 * b + b ^ 2 * c + c ^ 2 * a) * (a * b ^ 2 + b * c ^ 2 + c * a ^ 2) ≤ (a ^ 2 + b ^ 2 + c ^ 2) ^ 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph