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

22 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1991, Problem 3

Let S = {1, 2, ..., 280}. Find the smallest natural number n such that every n-element subset of S contains five numbers which are pairwise relatively prime.

Imports (2)

Imported by 1 file

Compfiles.lean

determine Imo1991P3.solution line 26 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
def Imo1991P3.badSet The elements of {1, ..., 280} divisible by 2, 3, 5 or 7 line 32 source
Source documentation
The elements of {1, ..., 280} divisible by 2, 3, 5 or 7. Among any five of them, two share a common prime factor.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Finset.filter, Or, Dvd.dvd, OfNat.ofNat, Finset.Icc
6 instances, coercions and auxiliary constants left out.
```
def badSet : Finset ℕ := (Finset.Icc 1 280).filter fun x => 2 ∣ x ∨ 3 ∣ x ∨ 5 ∣ x ∨ 7 ∣ x
```
def Imo1991P3.coprimeSet1 1 together with all primes in {1, ..., 280}; pairwise coprime line 35 source
Source documentation
1 together with all primes in {1, ..., 280}; pairwise coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def coprimeSet1 : Finset ℕ :=
…
```
def Imo1991P3.coprimeSet2 {2·41, 3·37, 5·31, 7·29, 11·23, 13·19}; pairwise coprime line 42 source
Source documentation
{2·41, 3·37, 5·31, 7·29, 11·23, 13·19}; pairwise coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def coprimeSet2 : Finset ℕ := {82, 111, 155, 203, 253, 247}
```
def Imo1991P3.coprimeSet3 {2·37, 3·31, 5·29, 7·23, 11·19, 13·17}; pairwise coprime line 45 source
Source documentation
{2·37, 3·31, 5·29, 7·23, 11·19, 13·17}; pairwise coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def coprimeSet3 : Finset ℕ := {74, 93, 145, 161, 209, 221}
```
def Imo1991P3.coprimeSet4 {2·31, 3·29, 5·23, 7·19, 11·17, 13·13}; pairwise coprime line 48 source
Source documentation
{2·31, 3·29, 5·23, 7·19, 11·17, 13·13}; pairwise coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def coprimeSet4 : Finset ℕ := {62, 87, 115, 133, 187, 169}
```
def Imo1991P3.coprimeSet5 {2·29, 3·23, 5·19, 7·17, 11·13}; pairwise coprime line 51 source
Source documentation
{2·29, 3·23, 5·19, 7·17, 11·13}; pairwise coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def coprimeSet5 : Finset ℕ := {58, 69, 95, 119, 143}
```
def Imo1991P3.coprimeSet6 {2·23, 3·19, 5·17, 7·13, 11·11}; pairwise coprime line 54 source
Source documentation
{2·23, 3·19, 5·17, 7·13, 11·11}; pairwise coprime.

standard axioms: Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Insert.insert, OfNat.ofNat, Singleton.singleton
4 instances, coercions and auxiliary constants left out.
```
def coprimeSet6 : Finset ℕ := {46, 57, 85, 91, 121}
```
def Imo1991P3.bigUnion The union of the six pairwise coprime families, all inside {1, ..., 280} line 57 source
Source documentation
The union of the six pairwise coprime families, all inside {1, ..., 280}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat
Proof uses: Union.union, Imo1991P3.coprimeSet1, Imo1991P3.coprimeSet2, Imo1991P3.coprimeSet3, Imo1991P3.coprimeSet4, Imo1991P3.coprimeSet5, Imo1991P3.coprimeSet6
2 instances, coercions and auxiliary constants left out.
```
def bigUnion : Finset ℕ :=
…
```
lemma Imo1991P3.bigUnion_card line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Finset.card, Imo1991P3.bigUnion, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.bigUnion_subset line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.bigUnion, Finset.Icc, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.coprimeSet1_pairwise line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.coprimeSet1, Ne, Eq, Nat.gcd, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.coprimeSet2_pairwise line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.coprimeSet2, Ne, Eq, Nat.gcd, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.coprimeSet3_pairwise line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.coprimeSet3, Ne, Eq, Nat.gcd, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.coprimeSet4_pairwise line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.coprimeSet4, Ne, Eq, Nat.gcd, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.coprimeSet5_pairwise line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.coprimeSet5, Ne, Eq, Nat.gcd, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.coprimeSet6_pairwise line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.coprimeSet6, Ne, Eq, Nat.gcd, OfNat.ofNat
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.five_of_subset If P ∩ T has at least 5 elements and the elements of P are pairwise coprime, then T contains five pairwise coprime numbers line 87 source
Source documentation
If P ∩ T has at least 5 elements and the elements of P are pairwise coprime, then T contains five pairwise coprime numbers.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, LE.le, OfNat.ofNat, Finset.card, Inter.inter, Membership.mem, Ne, Eq, Nat.gcd, Exists, And, Set.Pairwise, Nat.Coprime
Proof uses: Finset.exists_subset_card_eq, Exists.intro, And.intro, And.right, Iff.mp, Finset.mem_inter, Set, And.left, Eq.mp, congrArg, propext, Finset.mem_coe
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma five_of_subset {T P : Finset ℕ} (h : 5 ≤ (P ∩ T).card)
    (hp : ∀ a ∈ P, ∀ b ∈ P, a ≠ b → Nat.gcd a b = 1) :
    ∃ U ⊆ T, U.card = 5 ∧ (U : Set ℕ).Pairwise Nat.Coprime := by
…
```
Mentions: P, h
def Imo1991P3.smallPrimeFactor A prime in {2, 3, 5, 7} dividing x, whenever one exists line 97 source
Source documentation
A prime in {2, 3, 5, 7} dividing x, whenever one exists.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: ite, Dvd.dvd, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
def smallPrimeFactor (x : ℕ) : ℕ := if 2 ∣ x then 2 else if 3 ∣ x then 3 else if 5 ∣ x then 5 else 7
```
lemma Imo1991P3.smallPrimeFactor_mem line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Insert.insert, OfNat.ofNat, Singleton.singleton, Imo1991P3.smallPrimeFactor
Proof uses: id, dite, ite, Dvd.dvd, Eq.mpr, Eq, congrArg, ite_eq_left, of_eq_true, Eq.trans, Or, True, False, congr, eq_self, eq_false_of_decide, Eq.refl, Bool, Bool.false, or_self and 4 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1991P3.smallPrimeFactor_dvd line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Finset, Imo1991P3.badSet, Dvd.dvd, Imo1991P3.smallPrimeFactor
Proof uses: And, Finset.Icc, OfNat.ofNat, Or, Iff.mp, Finset.filter, Finset.mem_filter, id, dite, ite, Eq.mpr, Eq, congrFun', congrArg, ite_eq_left, Not, ite_eq_right, And.right, absurd
12 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
problem Imo1991P3.imo1991_p3 line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsLeast, Nat, Set.ofPred, Finset, LE.le, Finset.Icc, OfNat.ofNat, Eq, Finset.card, Exists, And, Set.Pairwise, Nat.Coprime, Imo1991P3.solution
Proof uses: Eq.mpr, id, congrArg, rfl, And.intro, Membership.mem, Set, lowerBounds, SDiff.sdiff, HSub.hSub, Finset.card_sdiff_of_subset, Eq.refl, Inter.inter, Imo1991P3.bigUnion, HAdd.hAdd, Finset.card_inter_add_card_sdiff, Eq.symm, Finset.card_le_card, Not, propext and 55 more
61 instances, coercions and auxiliary constants left out.

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