Claims

../

1977_11_01_erdos_newman: Theorem 2 of Erdős and Newman (1977) bounds below the smallest basis of most n-element subsets of [N]; glued along a dyadic sequence it gives a density-zero set with no basis of size o(N^{1/2}), a negative answer.

2025_12_25_barreto: A direct construction, posted on 2025-12-25 and formalized in Lean 4, of a density-zero set A lying in B+B for no B with counting function o(N^{1/2}); its Lean disproof was built here.

---