Prove2Me

lean_workbook_plus_394

Disproved

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

Prove that\n4∑cycab2c3+2∑cycbc5+2∑cyca2c4≥6a2b2c2+3∑cycabc4+3∑cyca3b34\sum_{cyc}a b^2 c^3 + 2\sum_{cyc}b c^5 + 2\sum_{cyc}a^2 c^4\geq 6a^2 b^2 c^2 + 3\sum_{cyc}a b c^4+ 3\sum_{cyc}a^3 b^3

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_394 : ∀ a b c : ℝ, 4 * (a * b^2 * c^3 + b * c^2 * a^3 + c * a^2 * b^3) + 2 * (b * c^5 + c * a^5 + a * b^5) + 2 * (a^2 * c^4 + b^2 * a^4 + c^2 * b^4) ≥ 6 * a^2 * b^2 * c^2 + 3 * (a * b * c^4 + b * c * a^4 + c * a * b^4) + 3 * (a^3 * b^3 + b^3 * c^3 + c^3 * a^3)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph