Erdős problem 26
Let be infinite. Must there exist some such that almost all integers have a divisor of the form for some ? 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 such that for every the set of multiples of has upper density below .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/26.leanFalse ↔ ∀ (A : ℕ → ℕ), StrictMono A → Erdos26.IsThick A → ∃ k, Erdos26.IsBehrend fun x => A x + kProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:26 - PLBY Lean proofs
ErdosProblems.Erdos26
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine
AI building on literature
- Machine
construction
- Machine
- Reported outcome