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
Let be an additive basis of order 2.
Must there exist which is also a basis such that does not exist?
True ↔ ∀ (A : Set ℕ), A.IsAddBasisOfOrder 2 → ∃ b, StrictMono b ∧ ∀ (n : ℕ), b n ∈ A ∧ (Set.range b).IsAddBasis ∧ ∀ (x : ℝ), ¬Filter.Tendsto (fun n => ↑(b n) / ↑n ^ 2) Filter.atTop (nhds x)OpenStatement only, no proof