Skip to content

Erdős problem 56

Start work

Suppose A⊆{1,…,N}A \subseteq \{1,\dots,N\} is such that there are no k+1k+1 elements of AA which are relatively prime. An example is the set of all multiples of the first kk primes. Is this the largest such set? To avoid trivial counterexamples, we must insist that NN be at least the kkth prime.

Sources

The source's own material, retained exactly.

11 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

56.lean

Retained formal statement2 of 11

Suppose A⊆{1,…,N}A \subseteq \{1,\dots,N\} is such that there are no k+1k+1 elements of AA which are relatively prime. An example is the set of all multiples of the first kk primes. Is this the largest such set? To avoid trivial counterexamples, we must insist that NN be at least the kkth prime.

FormalConjectures/ErdosProblems/56.leanErdos56.erdos_562 linesExact file
False ↔  ∀ 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.