Erdős Problem 56

Reference: erdosproblems.com/56

def 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

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

theorem weaklyDivisible_empty (k : ℕ) : WeaklyDivisible k ∅

theorem weaklyDivisible_one (k : ℕ) : WeaklyDivisible k {1}

noncomputable def MaxWeaklyDivisible (N k : ℕ) : ℕ

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

Equations

• MaxWeaklyDivisible N k = (Finset.filter (WeaklyDivisible k) (Finset.Icc 1 N).powerset).sup Finset.card

noncomputable def 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

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

theorem 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 erdos_56 (N : ℕ) : N ≥ 2 → ∀ (k : ℕ), 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?