lean_workbook_plus_13332

Disproved

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

Thus it suffices to show that \n\n

(b+c)^4-b^4-c^4-14b^2c^2=f(0, b, c)\ge 0

which becomes clear after expanding: \n\n

4bc(b-c)^2\ge 0.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13332 : ∀ b c : ℝ, (b + c) ^ 4 - b ^ 4 - c ^ 4 - 14 * b ^ 2 * c ^ 2 ≥ 0   :=  by sorry

Source