## 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.

Open with the in-brower editor at live.lean-lang.org: