Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1965P4

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1965, Problem 4

Find all sets of four real numbers x₁, x₂, x₃, x₄ such that the sum of any one
and the product of the other three is equal to 2.
-/

namespace Imo1965P4

/- determine -/ abbrev solution : Set (Multiset ℝ) := sorry

theorem imo1965_p4 : { S | S.card = 4 ∧ ∀ x ∈ S, x + (S.erase x).prod = 2 } = solution := sorry

end Imo1965P4

File author(s): Markus Rydh

This problem has a complete formalized solution.