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

10 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2024, Problem 1

Find all integers $n \geq 3$ such that the following property holds: if we list the divisors of $n!$ in increasing order as $1 = d_1 < d_2 < \cdots < d_k = n!$, then we have $d_2 - d_1 \leq d_3 - d_2 \leq \cdots \leq d_k - d_{k-1}$.

Imports (5)

Imported by 1 file

Compfiles.lean

def Usa2024P1.Good The property required of n: writing the divisors of n ! in increasing order as 1 = d₁ < d₂ < ⋯ < dₖ = n !, the consecutive gaps are non-decreasing line 37 source
Source documentation
The property required of n: writing the divisors of n ! in increasing order as 1 = d₁ < d₂ < ⋯ < dₖ = n !, the consecutive gaps are non-decreasing. We phrase this using consecutive triples: whenever a < b < c are divisors of n ! such that no divisor of n ! lies strictly between a and b, or strictly between b and c, we have b - a ≤ c - b. (Note: we write Nat.factorial n instead of n ! since the ! notation clashes with PiLp.vecNotation under a full Mathlib import.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Membership.mem, Finset, Nat.divisors, Nat.factorial, LT.lt, Or, LE.le, HSub.hSub
6 instances, coercions and auxiliary constants left out.
```
def Good (n : ℕ) : Prop :=
…
```
determine Usa2024P1.solution_set line 45 source
no axioms what this means
Statement uses: Set, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
3 instances, coercions and auxiliary constants left out.
lemma Usa2024P1.mul_dvd_factorial_of_ne If a and b are distinct positive integers with a, b ≤ n, then a * b ∣ Nat.factorial n: both occur as distinct factors in `n ! line 72 source
Source documentation
If a and b are distinct positive integers with a, b ≤ n, then a * b ∣ Nat.factorial n: both occur as distinct factors in n ! = ∏ i ∈ Finset.range n, (i + 1).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Ne, LE.le, Dvd.dvd, HMul.hMul, Nat.factorial
Proof uses: Membership.mem, Finset, Finset.range, HSub.hSub, Iff.mpr, Finset.mem_range, Finset.erase, And, Finset.mem_erase, And.intro, Eq, HAdd.hAdd, Finset.prod, Finset.mul_prod_erase, Eq.mpr, id, congrArg, Eq.symm, Finset.prod_range_add_one_eq_factorial, Eq.mp and 20 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma mul_dvd_factorial_of_ne {a b n : ℕ} (ha : 0 < a) (hb : 0 < b) (hab : a ≠ b)
    (han : a ≤ n) (hbn : b ≤ n) : a * b ∣ Nat.factorial n := by
…
```
lemma Usa2024P1.good_three The divisors of `3 ! line 85 source
Source documentation
The divisors of 3 ! = 6 are 1, 2, 3, 6, with gaps 1, 1, 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P1.Good, OfNat.ofNat, Nat
Proof uses: id, of_decide_eq_true, Membership.mem, Finset, Nat.divisors, Nat.factorial, LT.lt, Or, LE.le, HSub.hSub, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma good_three : Good 3 := by
…
```
Mentions: Usa2024P1.Good
lemma Usa2024P1.good_four The divisors of `4 ! line 91 source
Source documentation
The divisors of 4 ! = 24 are 1, 2, 3, 4, 6, 8, 12, 24, with gaps 1, 1, 1, 2, 2, 4, 12.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Usa2024P1.Good, OfNat.ofNat, Nat
Proof uses: id, of_decide_eq_true, Membership.mem, Finset, Nat.divisors, Nat.factorial, LT.lt, Or, LE.le, HSub.hSub, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma good_four : Good 4 := by
…
```
Mentions: Usa2024P1.Good
lemma Usa2024P1.not_good_five n = 5 fails: 15, 20, 24 are consecutive divisors of `5 ! line 97 source
Source documentation
n = 5 fails: 15, 20, 24 are consecutive divisors of 5 ! = 120, but 20 - 15 = 5 > 4 = 24 - 20.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Usa2024P1.Good, OfNat.ofNat, Nat
Proof uses: LE.le, HSub.hSub, of_decide_eq_true, Membership.mem, Finset, Nat.divisors, Nat.factorial, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Bool.false, Or, False.elim, False, Eq.mp and 3 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma not_good_five : ¬ Good 5 := by
…
```
Mentions: Usa2024P1.Good
lemma Usa2024P1.not_good_six n = 6 fails: 90, 120, 144 are consecutive divisors of `6 ! line 107 source
Source documentation
n = 6 fails: 90, 120, 144 are consecutive divisors of 6 ! = 720, but 120 - 90 = 30 > 24 = 144 - 120.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, Usa2024P1.Good, OfNat.ofNat, Nat
Proof uses: LE.le, HSub.hSub, of_decide_eq_true, Membership.mem, Finset, Nat.divisors, Nat.factorial, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Bool.false, Or, False.elim, False, Eq.mp and 3 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma not_good_six : ¬ Good 6 := by
…
```
Mentions: Usa2024P1.Good
lemma Usa2024P1.not_good_of_seven_le Documented declaration: not_good_of_seven_le line 117 source
Source documentation
Every n with 7 ≤ n ≤ 12 fails: 12, 14, 15 are consecutive divisors of n ! (there is no divisor strictly between 12 and 14 since 13 ∤ n !), but 14 - 12 = 2 > 1 = 15 - 14.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, Usa2024P1.Good
Proof uses: Dvd.dvd, Nat.factorial, Nat.factorial_dvd_factorial, Dvd.dvd.trans, of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, congrArg, propext, Nat.Prime.dvd_factorial, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_3 and 28 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma not_good_of_seven_le {n : ℕ} (h7 : 7 ≤ n) (hn12 : n ≤ 12) : ¬ Good n := by
…
```
Mentions: Usa2024P1.Good
lemma Usa2024P1.not_good_of_thirteen_le Every n ≥ 13 fails line 147 source
Source documentation
Every n ≥ 13 fails. With m = ⌊n / 2⌋ ≥ 6, both m² - 1 and m² divide n !, hence are consecutive divisors of n ! with gap 1. A downward induction using Good n then shows that every integer in [1, m²] divides n !, which contradicts Bertrand's postulate: there is a prime p with n < p ≤ 2n ≤ m².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, Usa2024P1.Good
Proof uses: And, HMul.hMul, HAdd.hAdd, Exists, False, Exists.intro, HDiv.hDiv, HPow.hPow, Eq, HSub.hSub, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 114 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 96 steps
Open to load the checked before-and-after goal states.
```
lemma not_good_of_thirteen_le {n : ℕ} (hn : 13 ≤ n) : ¬ Good n := by
…
```
Mentions: Usa2024P1.Good
problem Usa2024P1.usa2024_p1 line 225 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Iff, Membership.mem, Set, Usa2024P1.solution_set, Usa2024P1.Good
Proof uses: Iff.intro, Or, Eq, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congrArg, Usa2024P1.good_three, Eq.symm, Usa2024P1.good_four, Eq.mpr, id, And, Or.inl, rfl, Or.inr, absurd, Usa2024P1.not_good_five, Usa2024P1.not_good_six and 2 more
14 instances, coercions and auxiliary constants left out.

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