## Compfiles: Catalog Of Math Problems Formalized In Lean

## Imo1975P2

```
import Mathlib.Tactic
/-!
# International Mathematical Olympiad 1975, Problem 2
Let a1 < a2 < a3 < ... be positive integers.
Prove that for every i >= 1,
there are infinitely many a_n that can be written in the form a_n = ra_i + sa_j,
with r, s positive integers and j > i.
-/
namespace Imo1975P2
theorem imo1975_p2 (a : ℕ → ℤ)
(apos : ∀ i : ℕ, 0 < a i)
(ha : ∀ i : ℕ, a i < a (i + 1)) :
( ∀ i n0 : ℕ ,
∃ n, n0 ≤ n ∧
∃ r s : ℕ,
∃ j : ℕ,
a n = r * a i + s * a j ∧
i < j ∧
0 < r ∧
0 < s ):= sorry
end Imo1975P2
```

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: