Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 29

../

claims/: The 1 claim page of Problem 29, one per claimant's result; the problem's standing derives from them.


Statement. Is there an explicit construction of a set $A\subseteq \mathbb{N}$ such that A+A=NA+A=\mathbb{N} but 1A∗1A(n)=o(nϵ)1_A\ast 1_A(n)=o(n^\epsilon) for every ϵ>0\epsilon>0?

Formulation. The site does not define explicit; the page reads the word as [JPSZ24] do, as membership in AA testable in time polynomial in the number of digits.

Status. PROVED (LEAN), the site's label (page last edited 28 December 2025): Jain, Pham, Sawhney and Zakharov [JPSZ24] give an explicit set with A+A=NA+A=\mathbb{N} and 1A∗1A(n)≤Cnc/log⁡log⁡n1_A\ast1_A(n)\le Cn^{c/\log\log n}, so the answer is yes; the site's Lean marker corresponds to the proof the formal-conjectures catalog links, a third party's Lean proof of a weaker existence statement (see Formalization). The claim page [[problems/additive_bases/E0029/claims/2024_05_14_jain_pham_sawhney_zakharov|An explicit economical additive basis]] records the acceptance evidence: the refereed publication and the curator of erdosproblems.com, Thomas Bloom; the corpus has not built or audited the Lean proof.

Source. erdosproblems.com/29, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #29, https://www.erdosproblems.com/29.

References.

  • [JPSZ24] Jain, V. and Pham, H. T. and Sawhney, M. and Zakharov, D., An explicit economical additive basis. arXiv:2405.08650 (2024); Combin. Probab. Comput. 34 (2025), no. 6, 815--820, DOI 10.1017/S096354832510014X. Library home: jain_2024_explicit_economical_additive_basis.

Formalization. Statement in formal-conjectures, at its revision of 2026-09-19: tagged research solved with answer(True) and linking the Lean proof Erdos29.erdos_29 in Boris Alexeev's repository https://github.com/plby/lean-proofs. The catalog's statement and that theorem assert only that some AA has A+A=NA+A=\mathbb{N} and 1A∗1A(n)=o(nϵ)1_A\ast1_A(n)=o(n^\epsilon) for every ϵ>0\epsilon>0, which Erdős's probabilistic theorem already gives. As the catalog's docstring notes, the statement records only existence while the linked proof's witness is an explicit construction; explicitness is not formalized. The corpus has not built or audited the proof, so the label supplies no formal-verification credit; the claim page gives the pinned link.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.