Erdős problem 326
Does there exist which is a minimal basis of order (every large integer is the sum of elements from , and no proper subset of has this property) such that for some ? A claimed construction gives a minimal basis with , answering the question affirmatively; Erdős and Graham had conjectured a negative answer.
Sources
FormalConjectures/ErdosProblems/
326.lean
Retained formal statement
Erdős originally asked whether this was true with A = B, but this was disproved by Cassels.
∃ a, ∃ (_ : StrictMono a) (_ : (Set.range a).IsAddBasisOfOrder 2), ∃ x, ∃ (_ : 0 < x), Filter.Tendsto (fun n => ↑(a n) / ↑n ^ 2) Filter.atTop (nhds x)SolvedStatement only, no proof