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.