lean_workbook_plus_4843

Disproved

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

Thus, it remains to prove that ${4\left(\sqrt{\frac{a^2+b^2}{5}}\right)^5}\geq(a-b)a^2b^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4843 : ∀ a b : ℝ, (4 * (Real.sqrt ((a ^ 2 + b ^ 2) / 5)) ^ 5) ≥ (a - b) * a ^ 2 * b ^ 2   :=  by sorry

Source