Prove2Me

lean_workbook_plus_3637

Proved

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

Prove that 5(∑cyca2)2≥3∑cyca2bc+4(∑cyca2)(∑cycab)5(\sum_{cyc} a^2)^2\geq 3\sum_{cyc} a^2bc+4(\sum_{cyc} a^2)(\sum_{cyc} ab)

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

View graph