Prove2Me

lean_workbook_plus_72066

Proved

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

It is equivalent to 12[(a−b)6+(b−c)6+(c−a)6]+2[ab(a−b)4+bc(b−c)4+ca(c−a)4]+12(a4(b−c)2+b4(c−a)2+c4(a−b)2)≥0 \frac {1}{2}[(a - b)^6 + (b - c)^6 + (c - a)^6] + 2[ab(a - b)^4 + bc(b - c)^4 + ca(c - a)^4] + \frac {1}{2}(a^4(b-c)^2+b^4(c-a)^2+c^4(a-b)^2) \ge 0 .

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

View graph