Erdős problem 56 · problems.science

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.

Sources

Browse retained paths and inspect the exact material available for this Problem.

11 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

56.lean

Retained formal statement2 of 11

FormalConjectures/ErdosProblems/56.leanErdos56.erdos_562 linesExact file

1False ↔2  ∀ k > 0, ∀ N ≥ Nat.nth Nat.Prime (k - 1), Erdos56.MaxWeaklyDivisible N k = (Erdos56.FirstPrimesMultiples N k).card

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science