Prove2Me

lean_workbook_plus_79395

Proved

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

abc(ab+ac+bc)≤a3b2+b3c2+c3a2⇔∑cyc7a3b2≥7⋅∑cyca2b2c.abc(ab+ac+bc)\leq a^3b^2+b^3c^2+c^3a^2\Leftrightarrow\sum_{cyc}7a^3b^2\geq7\cdot\sum_{cyc}a^2b^2c. But ∑cyc7a3b2=∑cyc(4a3b2+2b3c2+c3a2)≥7⋅∑cyca12+2b8+6c4+37=7⋅∑cyca2b2c.\sum_{cyc}7a^3b^2=\sum_{cyc}(4a^3b^2+2b^3c^2+c^3a^2)\geq7\cdot\sum_{cyc}\sqrt[7]{a^{12+2}b^{8+6}c^{4+3}}=7\cdot\sum_{cyc}a^2b^2c.

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

View graph