lean_workbook_plus_6501

Disproved

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

Prove that $2(a^4+b^4)(b^4+c^4)(c^4+a^4) \geq (ab^2+bc^2+ca^2-abc)^4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6501 : ∀ a b c : ℝ, 2 * (a ^ 4 + b ^ 4) * (b ^ 4 + c ^ 4) * (c ^ 4 + a ^ 4) ≥ (a * b ^ 2 + b * c ^ 2 + c * a ^ 2 - a * b * c) ^ 4   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph