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

17 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2002, Problem 4

The positive divisors of the integer n > 1 are d₁ < d₂ < ... < dₖ, so that d₁ = 1 and dₖ = n. Let d = d₁d₂ + d₂d₃ + ... + dₖ₋₁dₖ. Show that d < n² and find all n for which d divides n².

Imports (17)

Imported by 1 file

Compfiles.lean

def Imo2002P4.nthDiv The i-th smallest positive divisor of n (meaningful for i < n.divisors.card) line 44 source
Source documentation
The i-th smallest positive divisor of n (meaningful for i < n.divisors.card).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: dite, LT.lt, Finset.card, Nat.divisors, OrderEmbedding, Fin, Finset.orderEmbOfFin, Fin.mk, Not, OfNat.ofNat
14 instances, coercions and auxiliary constants left out.
```
noncomputable def nthDiv (n i : ℕ) : ℕ :=
…
```
def Imo2002P4.pairSum The sum `d₁d₂ + d₂d₃ + line 48 source
Source documentation
The sum d₁d₂ + d₂d₃ + ... + dₖ₋₁dₖ over the ordered positive divisors of n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sum, Finset.range, HSub.hSub, Finset.card, Nat.divisors, OfNat.ofNat, HMul.hMul, Imo2002P4.nthDiv, HAdd.hAdd
8 instances, coercions and auxiliary constants left out.
```
noncomputable def pairSum (n : ℕ) : ℕ :=
…
```
lemma Imo2002P4.nthDiv_eq line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Finset.card, Nat.divisors, Eq, Imo2002P4.nthDiv, OrderEmbedding, Fin, Finset.orderEmbOfFin, rfl, Fin.mk
Proof uses: id, Eq.mpr, dite, Not, OfNat.ofNat, congrArg, dite_eq_left, Eq.refl
25 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P4.pairSum_eq line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Imo2002P4.pairSum, Finset.sum, Finset.range, HSub.hSub, Finset.card, Nat.divisors, OfNat.ofNat, HMul.hMul, Imo2002P4.nthDiv, HAdd.hAdd
Proof uses: rfl
8 instances, coercions and auxiliary constants left out.
lemma Imo2002P4.card_divisors_ge_two line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Finset.card, Nat.divisors
Proof uses: Finset, Insert.insert, Singleton.singleton, Membership.mem, Eq, Or, Eq.mp, Eq.trans, congrArg, Eq.mpr, id, Iff.mpr, And, Dvd.dvd, Ne, Nat.mem_divisors, And.intro, one_dvd, dvd_refl, Finset.card_le_card and 1 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P4.nthDiv_zero line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Imo2002P4.nthDiv
Proof uses: Finset.card, Nat.divisors, LE.le, Imo2002P4.card_divisors_ge_two, Eq.mpr, OrderEmbedding, Fin, Finset.orderEmbOfFin, rfl, Fin.mk, id, congrArg, Imo2002P4.nthDiv_eq, Finset.min', Iff.mp, Finset.Nonempty, Finset.card_pos, Eq.rec, Eq.symm, Finset.orderEmbOfFin_zero and 13 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P4.nthDiv_last line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, HSub.hSub, Finset.card, Nat.divisors, Eq, Imo2002P4.nthDiv
Proof uses: Eq.mpr, OrderEmbedding, Fin, Finset.orderEmbOfFin, rfl, Fin.mk, id, congrArg, Imo2002P4.nthDiv_eq, Finset.max', Iff.mp, Finset.Nonempty, Finset.card_pos, Eq.rec, Eq.symm, Nat.sub_lt, Nat.succ_pos, Finset.orderEmbOfFin_last, le_antisymm, Finset.max'_le and 12 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P4.nthDiv_ge line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset.card, Nat.divisors, LE.le, HAdd.hAdd, Imo2002P4.nthDiv
Proof uses: Nat.recAux, Eq.mpr, OrderEmbedding, Fin, Finset.orderEmbOfFin, rfl, Fin.mk, id, Eq, congrArg, Imo2002P4.nthDiv_eq, Nat.pos_of_mem_divisors, Finset.orderEmbOfFin_mem, OrderEmbedding.strictMono, Iff.mpr, Fin.lt_def, Nat.lt_succ_self, Nat.succ_le_of_lt, lt_of_le_of_lt, Eq.mp
25 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P4.div_lt_div_of_dvd_of_lt Division is strictly antitone on the divisors of a positive integer line 106 source
Source documentation
Division is strictly antitone on the divisors of a positive integer.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Dvd.dvd, HDiv.hDiv
Proof uses: LT.lt.trans, Nat.div_pos, Nat.le_of_dvd, Eq, HMul.hMul, Nat.mul_div_cancel', Decidable.byContradiction, Not, LE.le, mul_le_mul_right, Eq.mp, mul_lt_mul_of_pos_right
28 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma div_lt_div_of_dvd_of_lt {a b n : ℕ} (hn0 : 0 < n) (ha : a ∣ n) (hb : b ∣ n)
    (ha0 : 0 < a) (hab : a < b) : n / b < n / a := by
…
```
lemma Imo2002P4.nthDiv_pair Pairing of divisors: the i-th smallest times the i-th largest equals n line 119 source
Source documentation
Pairing of divisors: the i-th smallest times the i-th largest equals n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Finset.card, Nat.divisors, Eq, HMul.hMul, Imo2002P4.nthDiv, HSub.hSub
Proof uses: LE.le, Imo2002P4.card_divisors_ge_two, Fin, Fin.isLt, Membership.mem, Finset, HDiv.hDiv, OrderEmbedding, Finset.orderEmbOfFin, rfl, Fin.mk, Dvd.dvd, And.left, Ne, Iff.mp, And, Nat.mem_divisors, Finset.orderEmbOfFin_mem, Iff.mpr, And.intro and 17 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
lemma nthDiv_pair (n : ℕ) (hn : 1 < n) (i : ℕ) (hi : i < n.divisors.card) :
    nthDiv n i * nthDiv n (n.divisors.card - 1 - i) = n := by
…
```
Mentions: Imo2002P4.nthDiv
lemma Imo2002P4.nthDiv_one The second smallest divisor of n > 1 is its least prime factor line 167 source
Source documentation
The second smallest divisor of n > 1 is its least prime factor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Imo2002P4.nthDiv, Nat.minFac
Proof uses: LE.le, Finset.card, Nat.divisors, Imo2002P4.card_divisors_ge_two, Eq.mpr, OrderEmbedding, Fin, Finset.orderEmbOfFin, rfl, Fin.mk, id, congrArg, Imo2002P4.nthDiv_eq, le_antisymm, Membership.mem, Finset, Iff.mpr, And, Dvd.dvd, Ne and 23 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma nthDiv_one (n : ℕ) (hn : 1 < n) : nthDiv n 1 = n.minFac := by
…
```
Mentions: Imo2002P4.nthDiv
lemma Imo2002P4.tele Telescoping sum used in part (a) line 208 source
Source documentation
Telescoping sum used in part (a).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Rat, Finset.sum, Finset.range, HSub.hSub, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd
Proof uses: Finset.sum_range_sub', Eq.mpr, id, congrArg, Eq.mp, congr, Finset.sum_congr, Eq.refl, Finset, Membership.mem, congrFun', Eq.trans, Nat.cast_add, Nat.cast_one, Nat.cast_zero, of_eq_true, True, Inv.inv, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.instAddMonoidWithOne' and 12 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma tele (m : ℕ) :
    ∑ j ∈ Finset.range m, (1 / ((j : ℚ) + 1) - 1 / ((j : ℚ) + 1 + 1)) =
      1 - 1 / ((m : ℚ) + 1) := by
…
```
lemma Imo2002P4.pairSum_lt Part (a): the sum is less than n ^ 2 line 217 source
Source documentation
Part (a): the sum is less than n ^ 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Imo2002P4.pairSum, HPow.hPow
Proof uses: LE.le, Finset.card, Nat.divisors, Imo2002P4.card_divisors_ge_two, Rat, Eq, Finset.sum, Finset.range, HSub.hSub, HMul.hMul, Imo2002P4.nthDiv, HAdd.hAdd, Eq.mpr, id, congrArg, Imo2002P4.pairSum_eq, Eq.trans, Finset.sum_congr, Eq.refl, Finset and 160 more
181 instances, coercions and auxiliary constants left out.

Tactic trace: 90 steps
Open to load the checked before-and-after goal states.
```
lemma pairSum_lt (n : ℕ) (hn : 1 < n) : pairSum n < n ^ 2 := by
…
```
Mentions: Imo2002P4.pairSum
lemma Imo2002P4.pairSum_eq_of_prime line 325 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Nat.Prime, Eq, Imo2002P4.pairSum
Proof uses: Finset, Nat.divisors, Insert.insert, Singleton.singleton, Nat.Prime.divisors, Eq.mpr, Finset.sum, Finset.range, HSub.hSub, Finset.card, HMul.hMul, Imo2002P4.nthDiv, HAdd.hAdd, id, congrArg, Imo2002P4.pairSum_eq, Finset.card_pair, Ne, rfl, Finset.sum_range_one and 10 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma Imo2002P4.pairSum_not_dvd_of_not_prime Composite n does not work: n ^ 2 / n.minFac < d ≤ n ^ 2 / n.minFac line 340 source
Source documentation
Composite n does not work: n ^ 2 / n.minFac < d ≤ n ^ 2 / n.minFac.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, Nat.Prime, Imo2002P4.pairSum, HPow.hPow, Dvd.dvd, False
Proof uses: LE.le, Nat.minFac, Nat.Prime.two_le, Nat.minFac_prime, Ne, Eq, Or, eq_or_lt_of_le, Nat.minFac_le, absurd, Eq.rec, Finset.card, Nat.divisors, Finset, Insert.insert, Singleton.singleton, Membership.mem, Eq.mp, Eq.trans, congrArg and 57 more
85 instances, coercions and auxiliary constants left out.

Tactic trace: 104 steps
Open to load the checked before-and-after goal states.
```
lemma pairSum_not_dvd_of_not_prime (n : ℕ) (hn : 1 < n) (hnp : ¬ n.Prime)
    (ha : pairSum n < n ^ 2) (hdvd : pairSum n ∣ n ^ 2) : False := by
…
```
Mentions: Imo2002P4.pairSum
determine Imo2002P4.SolutionSet line 434 source
standard axioms: propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Nat.Prime
problem Imo2002P4.imo2002_p4 line 436 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, And, Imo2002P4.pairSum, HPow.hPow, Iff, Dvd.dvd, Membership.mem, Set, Imo2002P4.SolutionSet
Proof uses: And.intro, Imo2002P4.pairSum_lt, Iff.intro, Decidable.byContradiction, Nat.Prime, Not, Imo2002P4.pairSum_not_dvd_of_not_prime, Eq.mpr, id, Eq, congrArg, Imo2002P4.pairSum_eq_of_prime, dvd_pow_self, Ne, Mathlib.Meta.NormNum.isNat_eq_false, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false
20 instances, coercions and auxiliary constants left out.

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