lean_workbook_plus_78784
DisprovedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78784 : ∀ x y : ℝ, (8 * x * y - (x + y) ^ 2) ^ 2 - (x + y) ^ 4 ≤ 0 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_78784 : ∀ x y : ℝ, (8 * x * y - (x + y) ^ 2) ^ 2 - (x + y) ^ 4 ≤ 0 := by sorry