Erdős problem 56
Suppose is such that there are no elements of which are relatively prime. An example is the set of all multiples of the first primes. Is this the largest such set? To avoid trivial counterexamples, we must insist that be at least the th prime.
Sources
FormalConjectures/ErdosProblems/
56.lean
Retained formal statement
∀ {k : ℕ}, k ≠ 0 → Erdos56.MaxWeaklyDivisible 1 k = 1TestStatement only, no proof