lean_workbook_plus_64182

Disproved

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

Continue with nguoivn's approach in detailed: By Holder, we have: $(LHS)^2(\sum a(a+b))\ge (a+b+c)^3$ $\Longleftrightarrow (LHS)^2\ge \frac {(a+b+c)^3}{\sum a(a+b)}$ Hence so as to prove the inequality of the problem, it is enough to prove: $2(a+b+c)^3\ge 9(a^2+b^2+c^2+ab+bc+ca)$ , $(*)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64182 :
  ∀ a b c : ℝ,
    2 * (a + b + c) ^ 3 ≥ 9 * (a ^ 2 + b ^ 2 + c ^ 2 + a * b + b * c + c * a)   :=  by sorry

Source

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

View graph