56.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 10 curated AI-written annotations and 7190 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 project documentation, Formal Conjectures paper, arXiv v1

14 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 56

Reference: erdosproblems.com/56

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def Erdos56.WeaklyDivisible Say a set of natural numbers is k-weakly divisible if any k+1 elements of A are not relatively prime line 35 source
Source documentation
Say a set of natural numbers is k-weakly divisible if any k+1 elements of A are not relatively prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Not, Set.Pairwise, Nat.Coprime
6 instances, coercions and auxiliary constants left out.
```
def WeaklyDivisible (k : ℕ) (A : Finset ℕ) : Prop :=
…
```
lemma Erdos56.weaklyDivisible_empty line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos56.WeaklyDivisible, EmptyCollection.emptyCollection, Finset
Proof uses: of_eq_true, Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Not, Set.Pairwise, Nat.Coprime, Eq.trans, Eq, Finset.card, True, forall_congr, And, implies_congr, LE.le, congrFun', congrArg, Eq.refl, False and 4 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos56.weaklyDivisible_singleton A singleton is k-weakly divisible if k ≠ 0 line 44 source
Source documentation
A singleton is k-weakly divisible if k ≠ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Erdos56.WeaklyDivisible, Singleton.singleton, Finset
Proof uses: of_eq_true, Membership.mem, Finset.powersetCard, HAdd.hAdd, Not, Set.Pairwise, Nat.Coprime, Eq.trans, And, Eq, Finset.card, EmptyCollection.emptyCollection, True, Or, forall_congr, implies_congr, LE.le, congrFun', congrArg, Eq.refl and 9 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma weaklyDivisible_singleton {k : ℕ} (hk : k ≠ 0) (l : ℕ) : WeaklyDivisible k {l} := by
…
```
Mentions: Erdos56.WeaklyDivisible
lemma Erdos56.not_weaklyDivisible_zero No non-empty set is 1-weakly divisible line 49 source
Source documentation
No non-empty set is 1-weakly divisible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Finset.Nonempty, Not, Erdos56.WeaklyDivisible, OfNat.ofNat
Proof uses: Eq.mpr, Exists, And, LE.le, Eq, Finset.card, Set.Pairwise, Nat.Coprime, id, Eq.trans, congrArg, forall_congr, Membership.mem, Finset.powersetCard, HAdd.hAdd, implies_congr, congrFun', zero_add, Eq.refl, funext and 12 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma not_weaklyDivisible_zero {A : _} (h : A.Nonempty) : ¬WeaklyDivisible 0 A := by
…
```
Mentions: Erdos56.WeaklyDivisible
lemma Erdos56.empty_iff_weaklyDivisible_zero line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Nat, Iff, Erdos56.WeaklyDivisible, OfNat.ofNat, Eq, EmptyCollection.emptyCollection
Proof uses: Iff.intro, Iff.mp, Not, Finset.Nonempty, Finset.not_nonempty_iff_eq_empty, mt, Erdos56.not_weaklyDivisible_zero, Iff.mpr, Classical.not_not, Eq.rec, Erdos56.weaklyDivisible_empty, Eq.symm
4 instances, coercions and auxiliary constants left out.
def Erdos56.MaxWeaklyDivisible MaxWeaklyDivisible N k is the size of the largest k-weakly divisible subset of {1,..., N} line 60 source
Source documentation
MaxWeaklyDivisible N k is the size of the largest k-weakly divisible subset of {1,..., N}

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, Finset, LE.le, Finset.Icc, OfNat.ofNat, Erdos56.WeaklyDivisible, Eq, Finset.card
7 instances, coercions and auxiliary constants left out.
```
noncomputable def MaxWeaklyDivisible (N : ℕ) (k : ℕ) : ℕ :=
…
```
theorem Erdos56.maxWeaklyDivisible_zero line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos56.MaxWeaklyDivisible, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, Nat.find, True, Membership.mem, Set, Set.ofPred, And, Erdos56.WeaklyDivisible, EmptyCollection.emptyCollection, Finset, LE.le, DecidablePred, Exists, congrArg, funext, forall_congr, implies_congr, Eq.refl, implies_true and 22 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Erdos56.maxWeaklyDivisible_one line 69 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Eq, Erdos56.MaxWeaklyDivisible
Proof uses: Set, Set.ofPred, Exists, Finset, And, Erdos56.WeaklyDivisible, Or, EmptyCollection.emptyCollection, Singleton.singleton, Finset.card, Insert.insert, Set.ext, Iff.intro, Membership.mem, Eq.mpr, id, Eq.trans, congrArg, congrFun', of_eq_true and 32 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Erdos56.maxWeaklyDivisible_zero_k line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Erdos56.MaxWeaklyDivisible, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, SupSet.sSup, Set.ofPred, Exists, Finset, LE.le, Finset.Icc, Erdos56.WeaklyDivisible, Finset.card, Singleton.singleton, Set, funext, And, EmptyCollection.emptyCollection, propext, exists_prop_congr and 6 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Erdos56.FirstPrimesMultiples FirstPrimesMultiples N k is the set of numbers in {1,..., N} that are a multiple of one of the first k primes line 85 source
Source documentation
FirstPrimesMultiples N k is the set of numbers in {1,..., N} that are a multiple of one of the first k primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset
Proof uses: Finset.filter, Exists, And, LT.lt, Dvd.dvd, Nat.nth, Nat.Prime, Finset.Icc, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
noncomputable def FirstPrimesMultiples (N k : ℕ) : Finset ℕ :=
…
```
theorem Erdos56.firstPrimesMultiples_one_card_zero line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Erdos56.FirstPrimesMultiples, OfNat.ofNat
Proof uses: Eq.mpr, LT.lt, Not, Nat.nth, Nat.Prime, id, Eq.trans, Finset, ite, Exists, And, Singleton.singleton, EmptyCollection.emptyCollection, congrFun', congrArg, Finset.filter, Dvd.dvd, Finset.Icc, Finset.filter.congr_simp, Eq.refl and 16 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem Erdos56.firstPrimesMultiples_zero_k_card_zero line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Finset.card, Erdos56.FirstPrimesMultiples, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset, EmptyCollection.emptyCollection, Finset.filter, Exists, And, LT.lt, Dvd.dvd, Nat.nth, Nat.Prime, Finset.Icc, False, Finset.filter_congr, Membership.mem, Iff.of_eq, funext and 3 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Erdos56.weaklyDivisible_firstPrimesMultiples An example of a k-weakly divisible set is the subset of {1, ..., N} containing the multiples of the first k primes line 107 source
Source documentation
An example of a k-weakly divisible set is the subset of {1, ..., N} containing the multiples of the first k primes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos56.WeaklyDivisible, Erdos56.FirstPrimesMultiples
Proof uses: id, Finset, Membership.mem, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, Subtype, Fin, Exists, And, LT.lt, Dvd.dvd, Nat.nth, Nat.Prime, And.right, Finset.Icc, Iff.mp, Finset.filter, Finset.mem_filter, And.left and 38 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma weaklyDivisible_firstPrimesMultiples (N k : ℕ) :
    WeaklyDivisible k (FirstPrimesMultiples N k) := by
…
```
Mentions: Erdos56.WeaklyDivisible, Erdos56.FirstPrimesMultiples
theorem Erdos56.erdos_56 Suppose $A \subseteq \{1,\dots,N\}$ is such that there are no $k+1$ elements of $A$ which are relatively prime sorry line 152 source
Source documentation
Suppose $A \subseteq \{1,\dots,N\}$ is such that there are no $k+1$ elements of $A$ which are relatively prime. An example is the set of all multiples of the first $k$ primes. Is this the largest such set? To avoid trivial counterexamples, we must insist that $N$ be at least the $k$th prime.

depends on sorry what this means
Statement uses: Iff, False, Nat, GT.gt, OfNat.ofNat, GE.ge, Nat.nth, Nat.Prime, HSub.hSub, Eq, Erdos56.MaxWeaklyDivisible, Finset.card, Erdos56.FirstPrimesMultiples
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_56 : answer(False) ↔ ∀ᵉ (k > 0) (N ≥ (k-1).nth Nat.Prime),
    (MaxWeaklyDivisible N k = (FirstPrimesMultiples N k).card) := by
…
```
Mentions: Erdos56.MaxWeaklyDivisible, Erdos56.FirstPrimesMultiples