lean_workbook_plus_65053

Disproved

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

Prove that $a^4 + b^4 + c^4 \ge (a^3b + b^3a) + ( c^3a + a^3c) + (bc^3 + cb^3) \ge 2(a^2b^2 + b^2c^2 + c^2a^2)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65053 : ∀ a b c : ℝ, a ^ 4 + b ^ 4 + c ^ 4 ≥ (a ^ 3 * b + b ^ 3 * a) + (c ^ 3 * a + a ^ 3 * c) + (b * c ^ 3 + c * b ^ 3) ∧ (a ^ 3 * b + b ^ 3 * a) + (c ^ 3 * a + a ^ 3 * c) + (b * c ^ 3 + c * b ^ 3) ≥ 2 * (a ^ 2 * b ^ 2 + b ^ 2 * c ^ 2 + c ^ 2 * a ^ 2)   :=  by sorry

Source

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

View graph