lean_workbook_plus_55222
DisprovedProve :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55222 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → 4 * (a + b + c) ^ 3 > 27 * (a ^ 3 + b ^ 3 + c ^ 3) := by sorry
Source
Prove :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_55222 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → 4 * (a + b + c) ^ 3 > 27 * (a ^ 3 + b ^ 3 + c ^ 3) := by sorry