Prove2Me

lean_workbook_plus_61548

Proved

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

(Solution 1) a4+b4+c4≥abc(a+b+c)⇔(ab−bc)2+(ac−bc)2+(ab−ac)2≥0a^4 + b^4 + c^4 \geq abc(a+b+c) \Leftrightarrow (ab-bc)^2 + (ac-bc)^2 + (ab-ac)^2 \ge 0.

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

View graph