Erdős problem 26 · problems.science

Let $A\subset\mathbb{N}$ be infinite. Must there exist some $k\geq 1$ such that almost all integers have a divisor of the form $a+k$ for some $a\in A$ ? The question as posed follows negatively from Davenport–Erdős (1951). The AI result settles Tenenbaum's harder variant, also negatively: there is an infinite $A$ such that for every $k\geq 1$ the set of multiples of $A+k$ has upper density below $0.34$ .

Sources

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

11 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

26.lean

Retained formal statement3 of 10

Tenenbaum asked the weaker variant where for every $\epsilon>0$ there is some $k=k(\epsilon)$ such that at least $1-\epsilon$ density of all integers have a divisor of the form $a+k$ for some $a\in A$ .

The DeepMind prover agent has found a formal disproof of this statement.

FormalConjectures/ErdosProblems/26.leanErdos26.erdos_26.variants.tenenbaum1 lineExact file

1False ↔ ∀ (A : ℕ → ℕ), StrictMono A → Erdos26.IsThick A → ∀ ε > 0, ∃ k, Erdos26.IsWeaklyBehrend (fun x => A x + k) ε

SolvedProof has a holeformal conjecturesexternal 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