lean_workbook_plus_78080

Disproved

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

Multiply hung's $\sum_{cyc}\frac{ab(a+b)}{c^2} \ge 2(a+b+c)$ by $a^2b^2c^2$ to obtain $\sum_{sym}a^3b^4\ge\sum_{sym}a^3b^2c^2$ \n\n<=> $\sum a^3(b^2-c^2)^2\ge0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78080 : ∀ a b c : ℝ, (a^3 * (b^2 - c^2)^2 + b^3 * (c^2 - a^2)^2 + c^3 * (a^2 - b^2)^2 ≥ 0)   :=  by sorry

Source

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

View graph