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

8 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1986, Problem 1

(a) Do there exist 14 consecutive positive integers, each of which is divisible by a prime less than 13?

(b) Do there exist 21 consecutive positive integers, each of which is divisible by a prime less than 17?

Imports (5)

Imported by 1 file

Compfiles.lean

lemma Usa1986P1.prime_lt_thirteen_ne_two A prime less than 13 that is not 2 is one of 3, 5, 7, 11 line 34 source
Source documentation
A prime less than 13 that is not 2 is one of 3, 5, 7, 11.

standard axioms: propext what this means
Statement uses: Nat, Nat.Prime, LT.lt, OfNat.ofNat, Ne, Or, Eq
Proof uses: LE.le, Nat.Prime.two_le, dite, False.elim, Eq.mp, False, eq_false, Mathlib.Meta.NormNum.isNat_not_prime, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.not_prime_mul_of_ble, Bool, Bool.false, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Not and 17 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma prime_lt_thirteen_ne_two {p : ℕ} (hp : p.Prime) (h13 : p < 13) (h2 : p ≠ 2) :
    p = 3 ∨ p = 5 ∨ p = 7 ∨ p = 11 := by
…
```
lemma Usa1986P1.eq_of_dvd Documented declaration: eq_of_dvd line 44 source
Source documentation
If the same prime p ∈ {7, 11} divides both a + 2 * j₁ and a + 2 * j₂ with j₁, j₂ < 7, then j₁ = j₂: p divides 2 * (j₂ - j₁), which has absolute value less than 14, so it must be zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Or, And, Dvd.dvd, HAdd.hAdd, HMul.hMul, Eq
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_dvd (j₁ j₂ : ℕ) (a : ℕ) (h₁ : j₁ < 7) (h₂ : j₂ < 7)
    (h : (7 ∣ a + 2 * j₁ ∧ 7 ∣ a + 2 * j₂) ∨
         (11 ∣ a + 2 * j₁ ∧ 11 ∣ a + 2 * j₂)) :
    j₁ = j₂ := by
…
```
Mentions: h
lemma Usa1986P1.not_all_divisible_of_three Documented declaration: not_all_divisible_of_three line 57 source
Source documentation
Pigeonhole principle: among three pairwise distinct indices t₁, t₂, t₃ < 7, it cannot happen that each of a + 2 * t₁, a + 2 * t₂, a + 2 * t₃ is divisible by 7 or by 11 (two of them would share a prime, contradicting eq_of_dvd). Hence, if none of them is divisible by 3 or 5, one of them is divisible by none of 3, 5, 7, 11.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, LT.lt, OfNat.ofNat, And, Not, Dvd.dvd, HAdd.hAdd, HMul.hMul, Exists
Proof uses: dite, Or, absurd, Eq, Usa1986P1.eq_of_dvd, Or.inl, And.intro, Or.inr, Exists.intro, And.left, And.right, Iff.mp, not_or
17 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma not_all_divisible_of_three (t₁ t₂ t₃ : ℕ) (a : ℕ)
    (h₁₂ : t₁ ≠ t₂) (h₁₃ : t₁ ≠ t₃) (h₂₃ : t₂ ≠ t₃)
    (b₁ : t₁ < 7) (b₂ : t₂ < 7) (b₃ : t₃ < 7)
    (s₁ : ¬ 3 ∣ a + 2 * t₁ ∧ ¬ 5 ∣ a + 2 * t₁)
    (s₂ : ¬ 3 ∣ a + 2 * t₂ ∧ ¬ 5 ∣ a + 2 * t₂)
    (s₃ : ¬ 3 ∣ a + 2 * t₃ ∧ ¬ 5 ∣ a + 2 * t₃) :
    ∃ j < 7, ¬ 3 ∣ a + 2 * j ∧ ¬ 5 ∣ a + 2 * j ∧
             ¬ 7 ∣ a + 2 * j ∧ ¬ 11 ∣ a + 2 * j := by
…
```
lemma Usa1986P1.not_all_divisible Among any seven consecutive odd numbers a, a + 2, …, a + 12, at least one is divisible by none of the primes 3, 5, 7, 11 line 92 source
Source documentation
Among any seven consecutive odd numbers a, a + 2, …, a + 12, at least one is divisible by none of the primes 3, 5, 7, 11.
The proof follows the classical USAMO solution. At most three of the seven numbers are divisible by 3 (and if there are three, the two endpoints are among them), at most two by 5 (and then an endpoint is among them), at most one by 7 and at most one by 11, so at most six of the seven numbers can be divisible by one of 3, 5, 7, 11. We check the finitely many cases for a % 3 and a % 5: in each case three explicit indices avoid 3 and 5, and not_all_divisible_of_three finishes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Exists, And, LT.lt, OfNat.ofNat, Not, Dvd.dvd, HAdd.hAdd, HMul.hMul
Proof uses: HMod.hMod, Nat.mod_lt, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, dite, LE.le, Eq, Usa1986P1.not_all_divisible_of_three, Mathlib.Meta.NormNum.isNat_eq_false, And.intro, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Nat.zero_le
118 instances, coercions and auxiliary constants left out.

Tactic trace: 216 steps (first 200 of 216)
Open to load the checked before-and-after goal states.
```
lemma not_all_divisible (a : ℕ) :
    ∃ j < 7, ¬ 3 ∣ a + 2 * j ∧ ¬ 5 ∣ a + 2 * j ∧
             ¬ 7 ∣ a + 2 * j ∧ ¬ 11 ∣ a + 2 * j := by
…
```
determine Usa1986P1.does_exist_14 line 146 source
no axioms what this means
Statement uses: Bool
Proof uses: Bool.false
determine Usa1986P1.does_exist_21 line 148 source
no axioms what this means
Statement uses: Bool
Proof uses: Bool.true
problem Usa1986P1.usa1986_p1a line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ite, Eq, Bool, Usa1986P1.does_exist_14, Bool.true, Exists, Nat, And, LT.lt, OfNat.ofNat, Membership.mem, Finset, Finset.range, Nat.Prime, Dvd.dvd, HAdd.hAdd, Not
Proof uses: id, False, HSub.hSub, HMod.hMod, HMul.hMul, Usa1986P1.not_all_divisible, Iff.mpr, Finset.mem_range, Ne, Eq.rec, Eq.mp, congrArg, Eq.symm, Or, Usa1986P1.prime_lt_thirteen_ne_two
29 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
problem Usa1986P1.usa1986_p1b line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ite, Eq, Bool, Usa1986P1.does_exist_21, Bool.true, Exists, Nat, And, LT.lt, OfNat.ofNat, Membership.mem, Finset, Finset.range, Nat.Prime, Dvd.dvd, HAdd.hAdd, Not
Proof uses: id, Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool.false, dite, LE.le, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_minFac_2, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.isNat_dvd_true, Mathlib.Meta.NormNum.isNat_add, Eq.symm, le_antisymm, Nat.ge_of_not_lt, Mathlib.Tactic.IntervalCases.of_lt_right, Nat.rawCast, Eq.mp and 8 more
31 instances, coercions and auxiliary constants left out.

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