lean_workbook_plus_31325

Disproved

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

since $a^{2}+b^{2}+c^{2}\ge ab+bc+ca$ , we'll be done if we can show that\n $a^{5}+b^{5}+c^{5}+abc(a^{2}+b^{2}+c^{2})\ge a^{4}b+ab^{4}+b^{4}c+bc^{4}+c^{4}a+ca^{4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph