lean_workbook_plus_32289

Proved

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

Let $a,b$ be positive reals. Prove that \n ${{a}^{4}}+{{b}^{4}}+\frac{1}{4}\ge 2ab(1-ab)\Leftrightarrow 4{{({{a}^{2}}-{{b}^{2}})}^{2}}+{{(4ab-1)}^{2}}\ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32289 (a b : ℝ) : a^4 + b^4 + 1 / 4 ≥ 2 * a * b * (1 - a * b) ↔ 4 * (a^2 - b^2)^2 + (4 * a * b - 1)^2 ≥ 0   :=  by sorry

Source

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

View graph