Erdős Problem 56

Reference: erdosproblems.com/56

def Erdos56.WeaklyDivisible (k : ℕ) (A : Finset ℕ) : Prop

Say a set of natural numbers is k-weakly divisible if any k+1 elements of A are not relatively prime.

Equations

• Erdos56.WeaklyDivisible k A = ∀ s ∈ Finset.powersetCard (k + 1) A, ¬(↑s).Pairwise Nat.Coprime

theorem Erdos56.weaklyDivisible_empty (k : ℕ) : WeaklyDivisible k ∅

theorem Erdos56.weaklyDivisible_singleton {k : ℕ} (hk : k ≠ 0) (l : ℕ) : WeaklyDivisible k {l}

A singleton is k-weakly divisble if k ≠ 0.

theorem Erdos56.not_weaklyDivisible_zero {A : Finset ℕ} (h : A.Nonempty) : ¬WeaklyDivisible 0 A

No non-empty set is 1-weakly divisible.

theorem Erdos56.empty_iff_weaklyDivisible_zero {A : Finset ℕ} : WeaklyDivisible 0 A ↔ A = ∅

noncomputable def Erdos56.MaxWeaklyDivisible (N k : ℕ) : ℕ

MaxWeaklyDivisible N k is the size of the largest k-weakly divisible subset of {1,..., N}

Equations

• Erdos56.MaxWeaklyDivisible N k = sSup {x : ℕ | ∃ (A : Finset ℕ) (_ : A ⊆ Finset.Icc 1 N) (_ : Erdos56.WeaklyDivisible k A), A.card = x}

theorem Erdos56.maxWeaklyDivisible_zero (k : ℕ) : MaxWeaklyDivisible 0 k = 0

theorem Erdos56.maxWeaklyDivisible_one {k : ℕ} (hk : k ≠ 0) : MaxWeaklyDivisible 1 k = 1

theorem Erdos56.maxWeaklyDivisible_zero_k (N : ℕ) : MaxWeaklyDivisible N 0 = 0

noncomputable def Erdos56.FirstPrimesMultiples (N k : ℕ) : Finset ℕ

FirstPrimesMultiples N k is the set of numbers in {1,..., N} that are a multiple of one of the first k primes.

Equations

• Erdos56.FirstPrimesMultiples N k = Finset.filter (fun (i : ℕ) => ∃ j < k, Nat.nth Nat.Prime j ∣ i) (Finset.Icc 1 N)

theorem Erdos56.firstPrimesMultiples_one_card_zero (k : ℕ) : (FirstPrimesMultiples 1 k).card = 0

theorem Erdos56.firstPrimesMultiples_zero_k_card_zero (N : ℕ) : (FirstPrimesMultiples N 0).card = 0

theorem Erdos56.weaklyDivisible_firstPrimesMultiples (N k : ℕ) (hN : 1 ≤ N) : WeaklyDivisible k (FirstPrimesMultiples N k)

An example of a k-weakly divisible set is the subset of {1, ..., N} containing the multiples of the first k primes.

theorem Erdos56.erdos_56 : (∀ N ≥ 2, ∀ k > 0, MaxWeaklyDivisible N k = (FirstPrimesMultiples N k).card) ↔ False

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?