`Compfiles/Imo2015P6.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

15 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2015, Problem 6

The sequence $a_1, a_2, \dots$ of integers satisfies the conditions

$1 ≤ a_j ≤ 2015$ for all $j ≥ 1$,
$k + a_k ≠ l + a_l$ for all $1 ≤ k < l$. Prove that there exist two positive integers $b$ and $N$ for which $$\left|\sum_{j=m+1}^n (a_j-b)\right| ≤ 1007^2$$ for all integers $m,n$ such that $N ≤ m < n$.

Imports (3)

Imported by 1 file

Compfiles.lean

def Condition The conditions on a in the problem line 34 source
Source documentation
The conditions on a in the problem. We reindex a to start from 0 rather than 1; N then only has to be nonnegative rather than positive, and the sum in the problem statement is over Ico m n rather than Ioc m n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: And, Membership.mem, Finset, Finset.Icc, OfNat.ofNat, Function.Injective, HAdd.hAdd
9 instances, coercions and auxiliary constants left out.
```
def Condition (a : ℕ → ℤ) : Prop :=
…
```
def pool The collection of ball heights in the solution line 62 source
Source documentation
The collection of ball heights in the solution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Finset
2 instances, coercions and auxiliary constants left out.
```
def pool (a : ℕ → ℤ) : ℕ → Finset ℤ
  | 0 => ∅
  | t + 1 => (insert (a t) ((pool a t).erase 0)).map (Equiv.subRight (1 : ℤ))

variable {a : ℕ → ℤ} (ha : Condition a) {t : ℕ}

section Pool
```
Mentions: Condition
lemma exists_add_eq_of_mem_pool line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Membership.mem, Finset, pool, Exists, And, LT.lt, Eq, HAdd.hAdd
Proof uses: Nat.recAux, OfNat.ofNat, False.elim, Eq.mp, False, Insert.insert, Finset.erase, HSub.hSub, Equiv, Equiv.subRight, congrArg, funext, congrFun', Equiv.subRight_apply, Finset.map, Equiv.toEmbedding, Function.Embedding, Ne, Or, propext and 4 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma pool_subset_Icc The ball heights are always within [0, 2014] line 84 source
Source documentation
The ball heights are always within [0, 2014].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, LE.le, Finset, pool, Finset.Icc, OfNat.ofNat
Proof uses: Nat.recAux, of_eq_true, EmptyCollection.emptyCollection, Membership.mem, HAdd.hAdd, And, Insert.insert, Finset.erase, Eq, HSub.hSub, Exists, Eq.mp, Equiv, Equiv.subRight, congrArg, funext, congrFun', Equiv.subRight_apply, Finset.map, Equiv.toEmbedding and 13 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma pool_subset_Icc : pool a t ⊆ Finset.Icc 0 2014 := by
…
```
Mentions: pool
lemma not_mem_pool_self line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, Not, Membership.mem, Finset, pool
Proof uses: id, And, LT.lt, Eq, HAdd.hAdd, Exists, False, exists_add_eq_of_mem_pool, LT.lt.ne, And.right, Finset.Icc, OfNat.ofNat, Function.Injective
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma card_pool The number of balls stays unchanged if there is a ball with height 0 and increases by 1 otherwise line 104 source
Source documentation
The number of balls stays unchanged if there is a ball with height 0 and increases by 1 otherwise.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, Eq, Finset.card, pool, HAdd.hAdd, OfNat.ofNat, ite, Membership.mem, Finset
Proof uses: Not, Finset.erase, Eq.mpr, And, Ne, id, congrArg, propext, Finset.mem_erase, Or, not_and_or, Or.inr, not_mem_pool_self, Finset.map, Equiv.toEmbedding, Equiv.subRight, Insert.insert, Nat.succ, pool.eq_2, Finset.card_map and 14 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma card_pool : Finset.card (pool a (t + 1)) = Finset.card (pool a t) + if 0 ∈ pool a t then 0 else 1 := by
…
```
Mentions: pool
lemma monotone_card_pool line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, Monotone, Finset.card, pool
Proof uses: monotone_nat_of_le_succ, Eq, HAdd.hAdd, OfNat.ofNat, ite, Membership.mem, Finset, card_pool
11 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma exists_max_card_pool There exists a point where the number of balls reaches a maximum (which follows from its monotonicity and boundedness) line 118 source
Source documentation
There exists a point where the number of balls reaches a maximum (which follows from its monotonicity and boundedness). We take its coordinates for the problem's b and N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, Exists, GE.ge, Eq, Finset.card, pool
Proof uses: converges_of_monotone_of_bounded, monotone_card_pool, OfNat.ofNat, Eq.mp, LE.le, Finset.Icc, congrArg, Eq.trans, Int.toNat, HSub.hSub, HAdd.hAdd, Int.card_Icc, sub_zero, Finset.card_le_card, pool_subset_Icc
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma exists_max_card_pool : ∃ b N, ∀ t ≥ N, Finset.card (pool a t) = b :=
…
```
Mentions: pool
lemma b_pos line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, GE.ge, Eq, Finset.card, pool, LT.lt, OfNat.ofNat
Proof uses: Decidable.byContradiction, Not, False, LE.le, Or, le_or_gt, monotone_card_pool, Eq.mp, congrArg, propext, nonpos_iff_eq_zero, le_rfl, LT.lt.le, Eq.mpr, HAdd.hAdd, ite, Membership.mem, Finset, id, congrFun' and 11 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma zero_mem_pool line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, GE.ge, Eq, Finset.card, pool, Membership.mem, Finset, OfNat.ofNat
Proof uses: HAdd.hAdd, ite, card_pool, id, Eq.mp, Eq.trans, congr, congrArg, congrFun', LE.le, forall_congr, implies_congr, Eq.refl, Not, False, implies_congr_ctx
26 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma sum_sub_sum_eq_sub The key observation, one term of the telescoping sum for the problem's expression line 149 source
Source documentation
The key observation, one term of the telescoping sum for the problem's expression.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, GE.ge, Eq, Finset.card, pool, HSub.hSub, Finset.sum, HAdd.hAdd, OfNat.ofNat
Proof uses: id, Eq.mpr, Finset.map, Equiv.toEmbedding, Equiv.subRight, Insert.insert, Finset, Finset.erase, Function.Embedding, congrFun', congrArg, Finset.sum_map, Equiv, Finset.sum_congr, Eq.refl, Membership.mem, Equiv.subRight_apply, Not, And, Ne and 13 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma sum_sub_sum_eq_sub : ∑ x ∈ pool a (t + 1), x - ∑ x ∈ pool a t, x = a t - b := by
…
```
Mentions: pool
lemma sum_telescope The telescoping sum giving the part of the problem's expression within the modulus signs line 158 source
Source documentation
The telescoping sum giving the part of the problem's expression within the modulus signs.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, GE.ge, Eq, Finset.card, pool, LE.le, LT.lt, Finset.sum, Finset.Ico, HSub.hSub
Proof uses: Nat.le_induction, Nat.succ, Eq.mpr, id, congrArg, HAdd.hAdd, OfNat.ofNat, sum_sub_sum_eq_sub, of_eq_true, Eq.trans, True, congrFun', Singleton.singleton, Finset, Finset.sum_congr, Nat.Ico_succ_singleton, Membership.mem, Eq.refl, Finset.sum_sub_distrib, congr and 11 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma sum_telescope {m n : ℕ} (hm : N ≤ m) (hn : m < n) :
    ∑ j ∈ Finset.Ico m n, (a j - b) = ∑ x ∈ pool a n, x - ∑ x ∈ pool a m, x := by
…
```
Mentions: pool
lemma le_sum_pool line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, GE.ge, Eq, Finset.card, pool, LE.le, Finset.sum, Finset.range
Proof uses: Eq.mpr, HAdd.hAdd, OfNat.ofNat, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, id, congrArg, Membership.mem, zero_add, Finset.sum_range_le_sum, And.left, Iff.mp, Finset.Icc, And and 2 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma sum_pool_le line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, GE.ge, Eq, Finset.card, pool, LE.le, Finset.sum, Finset.range, HSub.hSub, OfNat.ofNat
Proof uses: Membership.mem, Finset, zero_mem_pool, Eq.mpr, Insert.insert, Finset.erase, id, congrArg, Eq.symm, Finset.insert_erase, HAdd.hAdd, Finset.sum_insert, Finset.notMem_erase, zero_add, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Finset.sum_congr and 10 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
problem Imo2015P6.imo2015_p6 line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Condition, Exists, And, GT.gt, OfNat.ofNat, GE.ge, LE.le, abs, Finset.sum, Finset.Ico, HSub.hSub, HPow.hPow
Proof uses: Eq, Finset.card, pool, exists_max_card_pool, LT.lt, b_pos, Exists.intro, And.intro, Iff.mpr, Int.natCast_pos, Eq.mpr, id, congrArg, sum_telescope, Trans.trans, HMul.hMul, Finset.range, abs_sub_le_of_le_of_le, le_sum_pool, LE.le.trans and 34 more
117 instances, coercions and auxiliary constants left out.

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