`Compfiles/Imo2021P1.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

4 declarations, 0 contain sorry, 0 declared as axioms

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.

Imports (4)

Imported by 1 file

Compfiles.lean

theorem Imo2021P1.exists_numbers_in_interval We will later make use of the fact that there exists (l : ℕ) such that n ≤ 2 * l ^ 2 - 4 * l and 2 * l ^ 2 + 4 * l ≤ 2 * n for n ≥ 100 line 61 source
Source comment
We will later make use of the fact that there exists (l : ℕ) such that n ≤ 2 * l ^ 2 - 4 * l and 2 * l ^ 2 + 4 * l ≤ 2 * n for n ≥ 100.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, And, HAdd.hAdd, HMul.hMul, HPow.hPow
Proof uses: Nat.sqrt, Eq.mpr, id, Eq, congrArg, propext, Nat.le_sqrt, Nat.sqrt_le', Nat.succ_le_succ_sqrt', HSub.hSub, Exists.intro, And.intro, Trans.trans, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq and 82 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem exists_numbers_in_interval (n : ℕ) (hn : 100 ≤ n) :
    ∃ l : ℕ, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n := by
…
```
theorem Imo2021P1.exists_triplet_summing_to_squares line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, And, LT.lt, HMul.hMul, Eq, HAdd.hAdd, HPow.hPow
Proof uses: Imo2021P1.exists_numbers_in_interval, Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, id, implies_congr, dite, Eq.symm, le_antisymm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.ge_of_not_lt, Nat.zero_le, Exists.intro, HSub.hSub, And.intro, Int and 88 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares Documented declaration: exists_finset_3_le_card_with_pairs_summing_to_squares line 92 source
Source comment
Since it will be more convenient to work with sets later on, we will translate the above claim to state that there always exists a set B ⊆ [n, 2n] of cardinality at least 3, such that each pair of pairwise unequal elements of B sums to a perfect square.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Finset, And, HAdd.hAdd, HMul.hMul, Finset.card, Membership.mem, Ne, Eq, HPow.hPow
Proof uses: LT.lt, Imo2021P1.exists_triplet_summing_to_squares, Exists.intro, Insert.insert, Singleton.singleton, And.intro, Not, Eq.mpr, Or, id, congrArg, propext, Finset.mem_insert, Finset.mem_singleton, congrFun', LT.lt.ne, LT.lt.trans, Finset.card_insert_of_notMem, And.left, And.right and 7 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem 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 ^ 2) ∧
      ∀ c ∈ B, n ≤ c ∧ c ≤ 2 * n := by
…
```
problem Imo2021P1.imo2021_p1 line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Finset, Finset.Icc, HMul.hMul, Or, Exists, Membership.mem, And, Ne, Eq, HAdd.hAdd, HPow.hPow, SDiff.sdiff
Proof uses: Finset.card, Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares, Eq.mpr, id, LT.lt, Union.union, Inter.inter, congrArg, Eq.symm, Finset.inter_union_distrib_left, Finset.sdiff_union_self_eq_union, Iff.mpr, Finset.union_eq_left, Finset.inter_eq_left, Iff.mp, Nat.succ, Nat.succ_le_iff, Finset.exists_subset_or_subset_of_two_mul_lt_card, Eq.mp, propext and 6 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.