lean_workbook_plus_77944
Disprovedprove that:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77944 : ∀ x y z : ℝ, (x * y) ^ 2 + (y * z) ^ 2 + (z * x) ^ 2 > (x ^ 4 + y ^ 4 + z ^ 4) / 2 := by sorry
Source
prove that:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_77944 : ∀ x y z : ℝ, (x * y) ^ 2 + (y * z) ^ 2 + (z * x) ^ 2 > (x ^ 4 + y ^ 4 + z ^ 4) / 2 := by sorry