Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1973P4

import Mathlib.Data.Complex.Basic

/-!
# USA Mathematical Olympiad 1973, Problem 4

Find all complex numbers x, y, z which satisfy
  x + y + z = x² + y² + z² = x³ + y³ + z³ = 3.
-/

namespace Usa1973P4

/- determine -/ abbrev solution_set : Set (ℂ × ℂ × ℂ) := sorry

theorem usa1973_p4 (x y z : ℂ) :
    x + y + z = 3 ∧
    x ^ 2 + y ^ 2 + z ^ 2 = 3 ∧
    x ^ 3 + y ^ 3 + z ^ 3 = 3 ↔ ⟨x,y,z⟩ ∈ solution_set := sorry

end Usa1973P4

File author(s): Shalev Wengrowsky

This problem does not yet have a complete formalized solution.