lean_workbook_plus_8456

Disproved

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

Prove that $abcd(a^{2}+b^{2}+c^{2}+d^{2}) \leqslant 4+\frac{3}{2} abcd (a+b+c+d)(a+b+c+d-4).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8456 : ∀ a b c d : ℝ, a * b * c * d * (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) ≤ 4 + 3 / 2 * a * b * c * d * (a + b + c + d) * (a + b + c + d - 4)   :=  by sorry

Source

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

View graph