Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2003P1

import Mathlib.Tactic

/-!
# International Mathematical Olympiad 2003, Problem 1

Let A be a 101-element subset of S = {1,2,...10⁶}. Prove that
there exist numbers t₁, t₂, ..., t₁₀₀ in S such that the sets

     Aⱼ = {x + tⱼ | x ∈ A},     j = 1,2, ..., 100

are pairwise disjoint.
-/

namespace Imo2003P1

abbrev S := Finset.Icc 1 1000000

theorem imo2003_p1 (A : Finset ℕ) (AS : A ⊆ S) (Acard : A.card = 101) :
    ∃ t ⊆ S, t.card = 100 ∧ ∀ x ∈ t, ∀ y ∈ t, x ≠ y → Disjoint {x + a | a ∈ A} {y + a | a ∈ A} := sorry

end Imo2003P1

File author(s): Ansar Azhdarov

This problem has a complete formalized solution.