`Compfiles/Imo2023P1.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 2023, Problem 1

Determine all composite integers n>1 that satisfy the following property: if d₁,d₂,...,dₖ are all the positive divisors of n with 1 = d₁ < d₂ < ... < dₖ = n, then dᵢ divides dᵢ₊₁ + dᵢ₊₂ for every 1 ≤ i ≤ k - 2.

Imports (2)

Imported by 1 file

Compfiles.lean

abbrev Imo2023P1.ConsecutiveFactors line 28 source
no axioms what this means
Statement uses: Nat
Proof uses: And, Dvd.dvd, LT.lt, Not, Exists
2 instances, coercions and auxiliary constants left out.
abbrev Imo2023P1.Dividable line 31 source
no axioms what this means
Statement uses: Nat
Proof uses: And, Imo2023P1.ConsecutiveFactors, Dvd.dvd, HAdd.hAdd
3 instances, coercions and auxiliary constants left out.
lemma Imo2023P1.PrimePow_ne Powers of distinct primes are never equal line 39 source
Source documentation
Powers of distinct primes are never equal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Ne, Exists, And, GT.gt, OfNat.ofNat, Eq, HPow.hPow
Proof uses: id, False, Finsupp, Nat.factorization, congrArg, Eq.rec, Eq.symm, Ne.symm, LT.lt.ne, Eq.mp, Finsupp.single, Finsupp.single_eq_of_ne, Finsupp.single_eq_same, Nat.Prime.factorization_pow
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma PrimePow_ne {a b p q : ℕ} (p_prime : p.Prime) (q_prime : q.Prime) (p_ne_q : p ≠ q)
    (ha : ∃ k > 0, p ^ k = a) (hb : ∃ k > 0, q ^ k = b)
    : a ≠ b := by
…
```
lemma Imo2023P1.dvd_ne_zero If a number divides some non-zero number, it is also nonzero line 53 source
Source documentation
If a number divides some non-zero number, it is also nonzero.

standard axioms: propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Dvd.dvd, LT.lt
Proof uses: Nat.zero_lt_of_ne_zero, Eq, Iff.mp, zero_dvd_iff, Eq.rec
11 instances, coercions and auxiliary constants left out.
```
lemma dvd_ne_zero {a b : ℕ} (hb : b ≠ 0) (h : a ∣ b) : 0 < a :=
…
```
Mentions: h
lemma Imo2023P1.dvd_n_fact_ne_zero If a prime p divides n, then n.factorization p ≠ 0 line 57 source
Source documentation
If a prime p divides n, then n.factorization p ≠ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Nat.Prime, Dvd.dvd, Finsupp, Nat.factorization
Proof uses: id, Eq, Or, Not, Iff.mp, Nat.factorization_eq_zero_iff, not_or_intro, not_not_intro
12 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_n_fact_ne_zero {n p : ℕ} (n_ne_0 : n ≠ 0) (p_prime : p.Prime) (p_dvd_n : p ∣ n)
    : n.factorization p ≠ 0 := by
…
```
lemma Imo2023P1.mul_cmp_compl Complementary factors are inversely ordered line 66 source
Source documentation
Complementary factors are inversely ordered.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMul.hMul
Proof uses: Nat.lt_of_mul_lt_mul_left, Eq.rec, Nat.mul_lt_mul_of_pos_right, Eq.symm
8 instances, coercions and auxiliary constants left out.
```
lemma mul_cmp_compl {a b x y : ℕ} (hab : a < b) (hy : 0 < y)
    (h : a * x = b * y) : y < x :=
…
```
Mentions: h
theorem Imo2023P1.p_succ_fact_zero Given prime p, the factorization of p + 1 is 0 at p line 72 source
Source documentation
Given prime p, the factorization of p + 1 is 0 at p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Eq, Finsupp, Nat.factorization, HAdd.hAdd, OfNat.ofNat
Proof uses: Nat.factorization_eq_zero_of_not_dvd, Function.comp, Dvd.dvd, False, Nat.Prime.not_dvd_one, Iff.mp, Nat.dvd_add_self_left
11 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem p_succ_fact_zero {p : ℕ} (hp : p.Prime)
    : (p + 1).factorization p = 0 := by
…
```
theorem Imo2023P1.not_pow_cons_factors_other_prime If p ^ e < c < p ^ (e + 1), then ∃ q prime that divides c line 78 source
Source documentation
If p ^ e < c < p ^ (e + 1), then ∃ q prime that divides c.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, GT.gt, HPow.hPow, LT.lt, HAdd.hAdd, OfNat.ofNat, Exists, And, Ne, Dvd.dvd
Proof uses: Classical.byContradiction, Not, Eq, Finsupp, Nat.factorization, Finsupp.single, Exists.intro, Finsupp.ext, dite, Eq.mpr, id, congrArg, Finsupp.single_eq_same, Eq.refl, Finsupp.single_eq_of_ne, Or.elim, em, Decidable.byContradiction, And.intro, Nat.dvd_of_factorization_pos and 14 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem not_pow_cons_factors_other_prime {p e c : ℕ} (hp : p.Prime)
    (c_gt_e : c > p ^ e) (c_lt_p_e_succ : c < p ^ (e + 1))
    : ∃ q ≠ p, q.Prime ∧ q ∣ c := by
…
```
theorem Imo2023P1.inv_cons_factors The inverse factors of consecutive factors of n are themselves consecutive factors of n line 110 source
Source documentation
The inverse factors of consecutive factors of n are themselves consecutive factors of n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, HMul.hMul, Imo2023P1.ConsecutiveFactors
Proof uses: Nat.zero_lt_of_ne_zero, And.right, Ne, Iff.mp, And, Nat.mul_ne_zero_iff, Ne.symm, Eq.rec, LT.lt.ne, Dvd.dvd, Not, Exists, Imo2023P1.mul_cmp_compl, And.intro, Exists.intro, Eq.mp, congrArg, Nat.mul_comm, id, False and 1 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem inv_cons_factors {n a b x y : ℕ} (hn : 0 < n) (ha : n = a * x)
    (hb : n = b * y) (h : ConsecutiveFactors n a b)
    : ConsecutiveFactors n y x := by
…
```
Mentions: h, Imo2023P1.ConsecutiveFactors
theorem Imo2023P1.factorization_prime If n.factorization p ≠ 0, then p is prime line 135 source
Source documentation
If n.factorization p ≠ 0, then p is prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, Finsupp, Nat.factorization, OfNat.ofNat, Nat.Prime
Proof uses: dite, Not, False.elim, Nat.factorization_eq_zero_of_not_prime
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem factorization_prime {n p : ℕ} (h : n.factorization p ≠ 0) : p.Prime := by
…
```
Mentions: h
theorem Imo2023P1.ordCompl_of_non_prime_pow If n is not a prime power, then its ordCompl[p] with respect to any p is > 1 line 142 source
Source documentation
If n is not a prime power, then its ordCompl[p] with respect to any p is > 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, IsPrimePow, GT.gt, HDiv.hDiv, HPow.hPow, Finsupp, Nat.factorization
Proof uses: Ne, Nat.ne_zero_of_lt, Decidable.byContradiction, Eq, LE.le, Nat.le_of_not_lt, Ne.symm, LT.lt.ne, Imo2023P1.dvd_ne_zero, Nat.ordCompl_dvd, Or.resolve_left, Iff.mp, Or, Nat.le_one_iff_eq_zero_or_eq_one, id, Eq.mpr, congrArg, Nat.factorization_one, Eq.refl, Nat.Prime and 30 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
theorem ordCompl_of_non_prime_pow {n p : ℕ} (hn : 1 < n) (hp : ¬IsPrimePow n)
    : ordCompl[p] n > 1 := by
…
```
theorem Imo2023P1.minFac_cons_factor If n is not a prime power, and p is its minimum factor, then the second smallest prime factor q is consecutive to p to some power > 0 line 196 source
Source documentation
If n is not a prime power, and p is its minimum factor, then the second smallest prime factor q is consecutive to p to some power > 0.
This theorem is key to solving the Dividable → PrimePower direction of the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Not, IsPrimePow, Exists, And, Nat.Prime, Ne, Nat.minFac, Imo2023P1.ConsecutiveFactors, HPow.hPow, HAdd.hAdd
Proof uses: Nat.ne_zero_of_lt, Nat.minFac_prime, Ne.symm, Nat.ne_of_lt, HDiv.hDiv, Finsupp, Nat.factorization, Eq, Finsupp.erase, congrArg, Nat.factorization_ordCompl, Dvd.dvd, Nat.ordCompl_dvd, Imo2023P1.ordCompl_of_non_prime_pow, Eq.mpr, id, Eq.symm, Eq.mp, Finsupp.erase_ne, Decidable.byContradiction and 76 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 92 steps
Open to load the checked before-and-after goal states.
```
theorem minFac_cons_factor {n : ℕ} (hn : 1 < n) (h : ¬IsPrimePow n)
    : ∃ q e,
      q.Prime ∧ q ≠ n.minFac ∧
      ConsecutiveFactors n (n.minFac ^ e) (n.minFac ^ (e + 1)) ∧
      ConsecutiveFactors n (n.minFac ^ (e + 1)) q := by
…
```
Mentions: h, Imo2023P1.ConsecutiveFactors
lemma Imo2023P1.PrimePow_cons_are_p_apart The consecutive factors of prime powers of p are a factor p apart line 342 source
Source documentation
The consecutive factors of prime powers of p are a factor p apart.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Exists, And, LT.lt, OfNat.ofNat, Eq, HPow.hPow, Imo2023P1.ConsecutiveFactors, HMul.hMul
Proof uses: Dvd.dvd, Not, LE.le, Iff.mp, Nat.dvd_prime_pow, Eq.rec, Eq.symm, Nat.pow_lt_pow_iff_right, Nat.Prime.one_lt, Eq.mpr, id, congrArg, HAdd.hAdd, Decidable.byContradiction, Nat.succ, Nat.lt_of_le_of_ne, Exists.intro, And.intro, Nat.exists_eq_add_of_lt, add_assoc and 7 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma PrimePow_cons_are_p_apart {x y p n : ℕ} (p_prime : p.Prime)
    (hn : ∃ k, 0 < k ∧ p ^ k = n) (h : ConsecutiveFactors n x y)
    : x * p = y := by
…
```
Mentions: h, Imo2023P1.ConsecutiveFactors
lemma Imo2023P1.PrimePow_is_dividable Proof that all prime powers are Dividable line 378 source
Source documentation
Proof that all prime powers are Dividable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, IsPrimePow, And, LT.lt, OfNat.ofNat, Imo2023P1.Dividable
Proof uses: And.intro, IsPrimePow.one_lt, Exists, Prime, Eq, HPow.hPow, Imo2023P1.ConsecutiveFactors, Dvd.dvd, HAdd.hAdd, HMul.hMul, Imo2023P1.PrimePow_cons_are_p_apart, Prime.nat_prime, Exists.intro, Eq.mpr, id, congrArg, Eq.symm, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl and 68 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma PrimePow_is_dividable {n : ℕ} : IsPrimePow n → 1 < n ∧ Dividable n := by
…
```
Mentions: Imo2023P1.Dividable
lemma Imo2023P1.dividable_is_PrimePow Proof that all Dividable numbers > 1 are prime powers line 391 source
Source documentation
Proof that all Dividable numbers > 1 are prime powers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, And, LT.lt, OfNat.ofNat, Imo2023P1.Dividable, IsPrimePow
Proof uses: Nat.minFac, Nat.Prime, Nat.minFac_prime, Ne.symm, Nat.ne_of_lt, Decidable.byContradiction, Not, Exists, Ne, Imo2023P1.ConsecutiveFactors, HPow.hPow, HAdd.hAdd, False, Imo2023P1.minFac_cons_factor, Dvd.dvd, Eq, HMul.hMul, Nat.zero_lt_of_lt, And.intro, Imo2023P1.inv_cons_factors and 37 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma dividable_is_PrimePow {n : ℕ} (h : 1 < n ∧ Dividable n)
    : IsPrimePow n := by
…
```
Mentions: h, Imo2023P1.Dividable
determine Imo2023P1.solution_set line 447 source
standard axioms: propext what this means
Statement uses: Set, Nat
Proof uses: Set.ofPred, And, Not, Nat.Prime, IsPrimePow
1 instances, coercions and auxiliary constants left out.
problem Imo2023P1.imo2023_p1 line 449 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Set, Nat, Imo2023P1.solution_set, Set.ofPred, And, LT.lt, OfNat.ofNat, Not, Nat.Prime, Imo2023P1.Dividable
Proof uses: Set.ext, Iff.intro, Membership.mem, IsPrimePow, Imo2023P1.PrimePow_is_dividable, And.intro, Imo2023P1.dividable_is_PrimePow
9 instances, coercions and auxiliary constants left out.

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