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

13 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1998, Problem 3

For any positive integer $n$, let $d(n)$ denote the number of positive divisors of $n$ (including 1 and $n$ itself). Determine all positive integers $k$ such that $d(n^2)/d(n) = k$ for some $n$.

Imports (6)

Imported by 1 file

Compfiles.lean

determine Imo1998P3.solution_set line 31 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, Exists, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
def Imo1998P3.d Define d(n), the function counting the number of positive divisors of n line 125 source
Source documentation
Define d(n), the function counting the number of positive divisors of n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Nat.divisors
```
def d (n : ℕ) : ℕ := (Nat.divisors n).card
```
lemma Imo1998P3.d_multiplicative Proof that d is multiplicative line 128 source
Source documentation
Proof that d is multiplicative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Coprime, Eq, Imo1998P3.d, HMul.hMul
Proof uses: Nat.Coprime.card_divisors_mul
2 instances, coercions and auxiliary constants left out.
```
lemma d_multiplicative (m n : ℕ) (h : Nat.Coprime m n) : d (m * n) = d m * d n :=
…
```
Mentions: h, Imo1998P3.d
lemma Imo1998P3.prime_power_divisors Proof that d(pᵏ) = k + 1 for p prime line 132 source
Source documentation
Proof that d(pᵏ) = k + 1 for p prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Eq, Imo1998P3.d, HPow.hPow, HAdd.hAdd, OfNat.ofNat
Proof uses: id, Eq.mpr, Finset.card, Nat.divisors, Finset.map, Function.Embedding.mk, Nat.pow_right_injective, Nat.Prime.two_le, Finset.range, congrArg, Finset, Nat.divisors_prime_pow, Finset.card_map, of_eq_true, Eq.trans, True, congrFun', Finset.card_range, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma prime_power_divisors {p k : ℕ} (hp : p.Prime) : d (p ^ k) = k + 1 := by
…
```
Mentions: Imo1998P3.d
lemma Imo1998P3.d_eq_dComputed Proof that d n = ∏ᵢ(kᵢ + 1) where n = ∏ᵢpᵢᵏᵢ (prime factorization), using the fact that d is multiplicative and d(pᵏ) = k + 1 for p prime line 142 source
Source documentation
Proof that d n = ∏ᵢ(kᵢ + 1) where n = ∏ᵢpᵢᵏᵢ (prime factorization), using the fact that d is multiplicative and d(pᵏ) = k + 1 for p prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, Imo1998P3.d, Finsupp.prod, Nat.factorization, HAdd.hAdd
Proof uses: Or, eq_or_ne, absurd, Eq.refl, Eq.symm, Eq.mpr, HPow.hPow, id, congrArg, Nat.multiplicative_factorization, Imo1998P3.d_multiplicative, of_eq_true, Eq.trans, True, congrFun', Finset.card, Nat.divisors, Singleton.singleton, Finset, Nat.divisors_one and 8 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma d_eq_dComputed (n : ℕ) (hn : n ≠ 0) : d n = n.factorization.prod (fun _ k ↦ k + 1) := by
…
```
Mentions: Imo1998P3.d
lemma Imo1998P3.d_n2 Proof that d(n²) = ∏ᵢ(2kᵢ + 1) for n = ∏ᵢpᵢᵏᵢ (prime factorization) line 151 source
Source documentation
Proof that d(n²) = ∏ᵢ(2kᵢ + 1) for n = ∏ᵢpᵢᵏᵢ (prime factorization).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, Imo1998P3.d, HPow.hPow, Finsupp.prod, Nat.factorization, HAdd.hAdd, HMul.hMul
Proof uses: Eq.mpr, id, congrArg, Imo1998P3.d_eq_dComputed, pow_ne_zero, HSMul.hSMul, Finsupp, Nat.factorization_pow, Finset.prod_congr, Finsupp.support, Finsupp.support_smul_eq, two_ne_zero, of_eq_true, Membership.mem, Finset, Nat.primeFactors, Eq.trans, True, forall_congr, And and 6 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma d_n2 (n : ℕ) (hn : n ≠ 0) : d (n ^ 2) = n.factorization.prod (fun _ k ↦ 2 * k + 1) := by
…
```
Mentions: Imo1998P3.d
lemma Imo1998P3.list_prod_odd Proof that if every number in a list is odd, the product of the list is odd line 159 source
Source documentation
Proof that if every number in a list is odd, the product of the list is odd.

standard axioms: Quot.sound, propext what this means
Statement uses: List, Nat, Membership.mem, Odd, List.prod
Proof uses: List.rec, of_eq_true, List.nil, OfNat.ofNat, Eq.trans, True, implies_congr, forall_congr, False, Eq.refl, implies_true, List.cons, Odd.mul, List.Mem.head, List.Mem.tail
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma list_prod_odd (l : List ℕ) : (∀ x ∈ l, Odd x) → Odd l.prod := by
…
```
theorem Imo1998P3.k_is_odd We begin by first proving that every value of k must be an odd number line 165 source
Source documentation
We begin by first proving that every value of k must be an odd number.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, And, Ne, OfNat.ofNat, Eq, Imo1998P3.d, HPow.hPow, HMul.hMul, HMod.hMod
Proof uses: Odd, Eq.mpr, Finsupp.prod, Nat.factorization, HAdd.hAdd, id, congrArg, Imo1998P3.d_n2, Finset.prod, Finsupp.support, Finsupp, Finsupp.prod.eq_1, Finset.prod_induction, Odd.mul, odd_one, Membership.mem, Finset, of_eq_true, Even, Iff.mp and 4 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem k_is_odd (k : ℕ)
    (h : ∃ n : ℕ, n ≠ 0 ∧ d (n ^ 2) = k * d n) :
    (k % 2 = 1) := by
…
```
Mentions: h, Imo1998P3.d
lemma Imo1998P3.exists_distinct_primes Proof that we can pick t new and distinct primes given a list of t primes line 177 source
Source documentation
Proof that we can pick t new and distinct primes given a list of t primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, List, Exists, And, Membership.mem, Nat.Prime, Not, Nat.Coprime, Eq, List.length, List.Nodup
Proof uses: Nat.recAux, Exists.intro, List.nil, of_eq_true, Eq.trans, True, congr, congrArg, forall_congr, False, implies_congr, Eq.refl, implies_true, eq_self, and_self, HAdd.hAdd, HAppend.hAppend, List.cons, List.concat_ne_nil, List.max and 76 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
lemma exists_distinct_primes (t n : ℕ) (hnneq0 : n ≠ 0) (primes : List ℕ) :
    (∃ l : List ℕ, (∀ i ∈ l, Nat.Prime i ∧ i ∉ primes ∧ Nat.Coprime i n)
        ∧ List.length l = t ∧ List.Nodup l) := by
…
```
lemma Imo1998P3.repeated_multiplicity_of_d Proof that d(∏ᵢxᵢ) = ∏ᵢd(xᵢ) for coprime xᵢ's (repeated mulitiplicity) line 232 source
Source documentation
Proof that d(∏ᵢxᵢ) = ∏ᵢd(xᵢ) for coprime xᵢ's (repeated mulitiplicity).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Nat, List.Pairwise, Nat.Coprime, Eq, Imo1998P3.d, List.prod, List.map
Proof uses: List.rec, List.nil, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, congrArg, Finset.card, Nat.divisors, Singleton.singleton, Finset, Nat.divisors_one, Finset.card_singleton, List.map_nil, eq_self, List.cons, Membership.mem, And, Eq.mp and 10 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma repeated_multiplicity_of_d (l : List ℕ) (hcoprime : l.Pairwise Nat.Coprime) :
    d (l.prod) = (List.map (fun i ↦ d i) l).prod := by
…
```
Mentions: Imo1998P3.d
lemma Imo1998P3.d_of_factorization Proof that d(∏ᵢpᵢᵏᵢ) = ∏ᵢ(kᵢ + 1) line 249 source
Source documentation
Proof that d(∏ᵢpᵢᵏᵢ) = ∏ᵢ(kᵢ + 1). Intuitively, we know ps and exps form a factorization of x, but Lean doesn't know this, so we have to give this lemma all the properties of x's factorization without explicitly saying so.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, List, Eq, List.length, Membership.mem, Nat.Prime, List.Nodup, GT.gt, OfNat.ofNat, Imo1998P3.d, List.prod, List.map, Prod, Imo1998P3.d_of_factorization.match_1, HPow.hPow, List.zip, HAdd.hAdd
Proof uses: Eq.mpr, Prod.fst, Prod.snd, id, congrArg, Imo1998P3.repeated_multiplicity_of_d, List.Nodup.pairwise_of_forall_ne, Nat.Coprime, List.Pairwise, Ne, propext, List.nodup_iff_pairwise_ne, List.pairwise_map, List.Pairwise.imp_of_mem, Prod.mk, And.left, List.of_mem_zip, And.right, dite, Not and 52 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 123 steps
Open to load the checked before-and-after goal states.
```
lemma d_of_factorization (t : ℕ) (ps exps : List ℕ)
    (hlen : ps.length = exps.length)
    (hlent : exps.length = t)
    (hallprime : ∀ i ∈ ps, Nat.Prime i)
    (hpsnodups : List.Nodup ps)
    (hexpsgt0 : ∀ i ∈ exps, i > 0) :
      d ((ps.zip exps).map (fun (p, e) ↦ p ^ e)).prod = (List.map (fun i ↦ i + 1) exps).prod := by
…
```
Mentions: Imo1998P3.d
theorem Imo1998P3.odd_k_satisfies We now prove that every odd number satisifies the equation line 361 source
Source documentation
We now prove that every odd number satisifies the equation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, HMod.hMod, OfNat.ofNat, Exists, And, Ne, Imo1998P3.d, HPow.hPow, HMul.hMul
Proof uses: Nat.strong_induction_on, LT.lt, Nat.casesAuxOn, False.elim, noConfusion_of_Nat, Nat.ctorIdx, HAdd.hAdd, dite, Eq.mpr, id, Exists.intro, congrArg, of_eq_true, Eq.trans, True, congr, congrFun', zero_add, one_pow, one_mul and 193 more
175 instances, coercions and auxiliary constants left out.

Tactic trace: 213 steps (first 200 of 213)
Open to load the checked before-and-after goal states.
```
theorem odd_k_satisfies (k : ℕ)
    (hkodd : k % 2 = 1) :
    (∃ n : ℕ, n ≠ 0 ∧ d (n ^ 2) = k * d n) := by
…
```
Mentions: Imo1998P3.d
problem Imo1998P3.imo1998_p3 line 573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Iff, Membership.mem, Set, Imo1998P3.solution_set, Exists, And, Ne, OfNat.ofNat, Eq, Finset.card, Nat.divisors, HPow.hPow, HMul.hMul
Proof uses: Iff.intro, HMod.hMod, Iff.mp, Odd, Nat.odd_iff, Iff.mpr, HAdd.hAdd, odd_iff_exists_bit1, Imo1998P3.d, Imo1998P3.odd_k_satisfies, Exists.intro, id, Imo1998P3.k_is_odd
33 instances, coercions and auxiliary constants left out.

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