## Compfiles: Catalog Of Math Problems Formalized In Lean

## Imo1995P2

```
import Mathlib.Tactic
/-!
# International Mathematical Olympiad 1995, Problem 2
Let a, b, c be positive real numbers such that abc = 1. Show that
1 / (a³(b + c)) + 1 / (b³(c + a)) + 1 / (c³(a + b)) ≥ 3/2.
-/
namespace Imo1995P2
open Finset
theorem imo1995_p2 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
(habc : a * b * c = 1) :
3 / 2 ≤ 1 / (a^3 * (b + c)) + 1 / (b^3 * (c + a)) + 1 / (c^3 * (a + b)) := sorry
end Imo1995P2
```

File author(s): Zheng Yuan

This problem has a complete formalized solution.

Open with the in-brower editor at live.lean-lang.org: