The board / number theory / #33
Erdős Problem #33
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Let `A ⊆ ℕ` be a set such that every integer can be written as `n^2 + a` for some `a` in `A` and `n ≥ 0`. -/ -- Formalisation note: Changed 'every large integer' to 'every integer' as for the statement these -- conditions are equivalent. Also, this was the formulation in the original paper `by Erdos. def AdditiveBasisCondition (A : Set ℕ) : Prop := ∀ (k : ℕ), ∃ (n : ℕ) (a : ℕ), a ∈ A ∧ k = a + n^2 def erdos_33.answer : EReal := sorry /-- Let `A ⊆ ℕ` be a set such that every integer can be written as `n^2 + a` for some `a` in `A` and `n ≥ 0`. What is the smallest possible value of `lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2)`?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/33.Prizenone
Topicsnumber theory, additive basis
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/33
Attempts
submit one →Read our working report →
exact finite square-completion numbers are verified through target 101, with a rigorous block reduction isolating the missing uniform \(q(N)<(2-o(1))\sqrt N\) lemma; the live limsup constant remains o
PARTIAL