Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1983P5

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 1983, Problem 5

Is it possible to choose $1983$ distinct positive integers,
all less than or equal to $10^5$,
no three of which are consecutive terms of an arithmetic progression?
Justify your answer.
-/

namespace Imo1983P5

theorem imo1983_p5 :
  ∃ S : Finset ℕ, S.card = 1983 ∧
  (∀ x ∈ S, x ≤ 10^5) ∧
  ∀ x ∈ S, ∀ y ∈ S, ∀ z ∈ S, x < y ∧ y < z → x + z ≠ 2 * y := sorry


end Imo1983P5

File author(s): InternLM-MATH LEAN Formalizer v0.1

This problem does not yet have a complete formalized solution.