Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2004P5

import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2004, Problem 5

Prove that for a,b,c > 0,
(a⁵ - a² + 3) (b⁵ - b² + 3) (c⁵ - c² + 3) ≥ (a + b + c)³.
-/

namespace Usa2004P5

theorem usa2004_p5 {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    (a + b + c) ^ 3 ≤ (a^5 - a^2 + 3) * (b^5 - b^2 + 3) * (c^5 - c^2 + 3) := sorry
end Usa2004P5

File author(s): Evan Chen

This problem has a complete formalized solution.