Compfiles: Catalog Of Math Problems Formalized In Lean

Imo2021P1

import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Tactic.IntervalCases
import Mathlib.Tactic.Linarith

/-!
# International Mathematical Olympiad 2021, Problem 1

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.
-/

namespace Imo2021P1

theorem imo2021_p1 :
    ∀ n : ℕ, 100 ≤ n → ∀ (A) (_ : A ⊆ Finset.Icc n (2 * n)),
    (∃ (a : _) (_ : a ∈ A) (b : _) (_ : b ∈ A), a ≠ b ∧ ∃ k : ℕ, a + b = k ^ 2) ∨
    ∃ (a : _) (_ : a ∈ Finset.Icc n (2 * n) \ A) (b : _) (_ : b ∈ Finset.Icc n (2 * n) \ A),
      a ≠ b ∧ ∃ k : ℕ, a + b = k ^ 2 := sorry


end Imo2021P1

File author(s): Mantas Bakšys

This problem has a complete formalized solution.

The solution was imported from mathlib4/Archive/Imo/Imo2021Q1.lean.