Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1971P1

import Mathlib.Tactic
import Mathlib.Data.Fin.Tuple.Sort

/-!
# International Mathematical Olympiad 1971, Problem 1

Prove that the following assertion is true for n = 3 and n = 5, and that it is
false for every other natural number n > 2:

If a1, a2, ..., an are arbitrary real numbers, then
(a1 − a2)(a1 − a3) · · · (a1 − an) + (a2 − a1)(a2 − a3) · · · (a2 − an)
+ · · · + (an − a1)(an − a2) · · · (an − an−1) ≥ 0
-/

namespace Imo1971P1

def E {n : ℕ} (a : Fin n → ℝ) : ℝ :=
  ∑ i, ∏ j ≠ i, (a i - a j)

def P (n : ℕ) : Prop :=
  ∀ (a : Fin n → ℝ), E a ≥ 0

theorem imo1971_p1 : P 3 ∧ P 5 ∧ ∀ n > 2, n ≠ 3 ∧ n ≠ 5 → ¬P n := sorry


end Imo1971P1

File author(s): Francesco Cappetti

This problem has a complete formalized solution.