Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1997P5

import Mathlib.Analysis.SpecialFunctions.Pow.Real

/-!
# USA Mathematical Olympiad 1997, Problem 5

Let a, b, c be positive reals.
Prove that
1 / (a³ + b³ + abc) + 1 / (b³ + c³ + abc) + 1 / (c³ + a³ + abc) ≤ 1 / abc
-/

open Real

namespace Usa1997P5

variable {a b c : ℝ}

theorem usa1997_p5 (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    1 / (a^3 + b^3 + a*b*c) + 1 / (b^3 + c^3 + a*b*c) + 1 / (c^3 + a^3 + a*b*c) ≤ 1 / (a*b*c) := sorry -- RHS of main sum = RHS of desired

end Usa1997P5

File author(s): Evan Chen

This problem has a complete formalized solution.