## Compfiles: Catalog Of Math Problems Formalized In Lean

## Imo1974P5

```
import Mathlib.Tactic
/-!
# International Mathematical Olympiad 1974, Problem 5
What are the possible values of
a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
as a,b,c,d range over the positive real numbers?
-/
namespace Imo1974P5
/- determine -/ abbrev solution_set : Set ℝ := sorry
theorem imo1974_p5 (s : ℝ) :
s ∈ solution_set ↔
∃ a b c d : ℝ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧
s = a / (a + b + d) + b / (a + b + c) +
c / (b + c + d) + d / (a + c + d) := sorry
end Imo1974P5
```

File author(s): David Renshaw

This problem has a complete formalized solution.

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