Skip to content

Erdős problem 26

Let A⊂NA\subset\mathbb{N} be infinite. Must there exist some k≥1k\geq 1 such that almost all integers have a divisor of the form a+ka+k for some a∈Aa\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 AA such that for every k≥1k\geq 1 the set of multiples of A+kA+k has upper density below 0.340.34.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/26.lean

Formal Conjectures

FormalConjectures/ErdosProblems/26.leanErdos26.erdos_261 lineExact file
False ↔ ∀ (A : ℕ → ℕ), StrictMono A → Erdos26.IsThick A → ∃ k, Erdos26.IsBehrend fun x => A x + k
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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:26
  • PLBY Lean proofsErdosProblems.Erdos26

Reported activity

Reported by these sources. Not reviewed here.

Continue