Prove2Me

lean_workbook_plus_73943

Disproved

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

For all real a, b, c prove that:\n\n

a4+b4+c4+4a2c2+4b2c2+4c2a2+a2+b2+c2≥2a3(b+c)+2b3(a+c)+2c3(a+b)+6abca^4+b^4+c^4+4a^2c^2+4b^2c^2+4c^2a^2+a^2+b^2+c^2 \ge 2a^3(b+c)+2b^3(a+c)+2c^3(a+b)+6abc
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73943 : ∀ a b c : ℝ, a ^ 4 + b ^ 4 + c ^ 4 + 4 * a ^ 2 * c ^ 2 + 4 * b ^ 2 * c ^ 2 + 4 * c ^ 2 * a ^ 2 + a ^ 2 + b ^ 2 + c ^ 2 ≥ 2 * a ^ 3 * (b + c) + 2 * b ^ 3 * (a + c) + 2 * c ^ 3 * (a + b) + 6 * a * b * c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph