Compfiles: Catalog Of Math Problems Formalized In Lean

Imo1975P2

import Mathlib.Tactic
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Int.Basic
import Mathlib.Data.Finset.Basic

/-!
# 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, Shahar Blumentzvaig

This problem has a complete formalized solution.