IMO 2021 Q1

Let n ≥ 100 be an integer. Ivan writes the numbers n, n+1, ..., 2*n 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 ^ 2 - 4 * l
b = 2 * l ^ 2 + 1
c = 2 * l ^ 2 + 4 * l

Therefore, it is enough to show that there exists a natural number l such that n ≤ 2 * l ^ 2 - 4 * l and 2 * l ^ 2 + 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.

theorem Imo2021Q1.exists_numbers_in_interval {n : ℕ} (hn : 100 ≤ n) : ∃ (l : ℕ), n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n

theorem Imo2021Q1.exists_triplet_summing_to_squares {n : ℕ} (hn : 100 ≤ n) : ∃ (a : ℕ) (b : ℕ) (c : ℕ), n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ IsSquare (a + b) ∧ IsSquare (c + a) ∧ IsSquare (b + c)

theorem Imo2021Q1.exists_finset_3_le_card_with_pairs_summing_to_squares {n : ℕ} (hn : 100 ≤ n) : ∃ (B : Finset ℕ), 2 * 1 + 1 ≤ B.card ∧ (∀ a ∈ B, ∀ b ∈ B, a ≠ b → IsSquare (a + b)) ∧ ∀ c ∈ B, n ≤ c ∧ c ≤ 2 * n

theorem imo2021_q1 (n : ℕ) : 100 ≤ n → ∀ A ⊆ Finset.Icc n (2 * n), (∃ a ∈ A, ∃ b ∈ A, a ≠ b ∧ IsSquare (a + b)) ∨ ∃ a ∈ Finset.Icc n (2 * n) \ A, ∃ b ∈ Finset.Icc n (2 * n) \ A, a ≠ b ∧ IsSquare (a + b)