Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1966P5

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1966, Problem 5

Solve the system of equations

  |a_1 - a_2| x_2 +|a_1 - a_3| x_3 +|a_1 - a_4| x_4 = 1
  |a_2 - a_1| x_1 +|a_2 - a_3| x_3 +|a_2 - a_4| x_4 = 1
  |a_3 - a_1| x_1 +|a_3 - a_2| x_2 +|a_3 - a_4| x_4 = 1
  |a_4 - a_1| x_1 +|a_4 - a_2| x_2 +|a_4 - a_3| x_3 = 1

  where a_1, a_2, a_3, a_4 are four different real numbers.
-/

namespace Imo1966P5

noncomputable /- determine -/ abbrev solution_set {a : Fin 4 → ℝ}
    (ha : Function.Injective a) : Set ((Fin 4 → ℝ)) := sorry

theorem imo1966_p5
    (x a : Fin 4 → ℝ)
    (ha : Function.Injective a) :
    (∀ i : Fin 4, ∑ j : Fin 4, abs (a i - a j) * x j = 1)
    ↔ x ∈ solution_set ha := sorry

end Imo1966P5

File author(s): Roozbeh Yousefzadeh, Benpigchu

This problem has a complete formalized solution.

The solution was imported from IMO-Steps/Lean_v20/imo_proofs/imo_1966_p5.lean.