lean_workbook_plus_56872

Disproved

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

After clearing denominators and squaring both sides the inequality becomes: $(a^3+b^3+c^3)(ab+bc+ca)^2\ge 3a^2b^2c^2(\sqrt{a}+\sqrt{b}+\sqrt{c})^2$ (*)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56872 :
    ∀ a b c : ℝ, (a^3 + b^3 + c^3) * (a * b + b * c + c * a)^2 ≥
    3 * a^2 * b^2 * c^2 * (Real.sqrt a + Real.sqrt b + Real.sqrt c)^2   :=  by sorry

Source

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

View graph