IMO 2021 Q1 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Let n≥100 be an integer. Ivan writes the numbers n, n+1,..., 2n each on different cards. He then shuffles these n+1 cards, and divides them into two piles. Prove that at least one of the piles contains two cards such that the sum of their numbers is a perfect square.

Solution #

We show there exists a triplet a, b, c ∈ [n , 2n] with a < b < c and each of the sums (a + b), (b + c), (a + c) being a perfect square. Specifically, we consider the linear system of equations

a + b = (2 * l - 1) ^ 2
a + c = (2 * l) ^ 2
b + c = (2 * l + 1) ^ 2

which can be solved to give

a = 2 * l * l - 4 * l
b = 2 * l * l + 1
c = 2 * l * l + 4 * l

Therefore, it is enough to show that there exists a natural number l such that n ≤ 2 * l * l - 4 * l and 2 * l * l + 4 * l ≤ 2 * n for n ≥ 100.

Then, by the Pigeonhole principle, at least two numbers in the triplet must lie in the same pile, which finishes the proof.

source

theorem imo2021_q1.lower_bound (n l : ℕ) (hl : 2 + √ (4 + 2 * ↑n) ≤ 2 * ↑l) :

n + 4 * l ≤ 2 * l * l

source

theorem imo2021_q1.upper_bound (n l : ℕ) (hl : ↑l ≤ √ (1 + ↑n) - 1) :

2 * l * l + 4 * l ≤ 2 * n

source

theorem imo2021_q1.radical_inequality {n : ℕ} (h : 107 ≤ n) :

√ (4 + 2 * ↑n) ≤ 2 * (√ (1 + ↑n) - 3)

source

theorem imo2021_q1.exists_numbers_in_interval (n : ℕ) (hn : 107 ≤ n) :

∃ (l : ℕ), n + 4 * l ≤ 2 * l * l ∧ 2 * l * l + 4 * l ≤ 2 * n

source

theorem imo2021_q1.exists_triplet_summing_to_squares (n : ℕ) (hn : 100 ≤ n) :

∃ (a b c : ℕ), n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ (k : ℕ), a + b = k * k) ∧ (∃ (l : ℕ), c + a = l * l) ∧ ∃ (m : ℕ), b + c = m * m

source

theorem imo2021_q1.exists_finset_3_le_card_with_pairs_summing_to_squares (n : ℕ) (hn : 100 ≤ n) :

∃ (B : finset ℕ), 2 * 1 + 1 ≤ B.card ∧ (∀ (a : ℕ), a ∈ B → ∀ (b : ℕ), b ∈ B → a ≠ b → (∃ (k : ℕ), a + b = k * k)) ∧ ∀ (c : ℕ), c ∈ B → n ≤ c ∧ c ≤ 2 * n

source

theorem imo2021_q1 (n : ℕ) :

100 ≤ n → ∀ (A : finset ℕ), A ⊆ finset.Icc n (2 * n) → ((∃ (a : ℕ) (H : a ∈ A) (b : ℕ) (H : b ∈ A), a ≠ b ∧ ∃ (k : ℕ), a + b = k * k) ∨ ∃ (a : ℕ) (H : a ∈ finset.Icc n (2 * n) \ A) (b : ℕ) (H : b ∈ finset.Icc n (2 * n) \ A), a ≠ b ∧ ∃ (k : ℕ), a + b = k * k)