---

Claim. The answer is yes. Theorem 2 of B. Green, The Cameron-Erdős conjecture, Bull. London Math. Soc. 36 (2004), no. 6, 769--778, states that the number of sum-free subsets of $\{1,\ldots,n\}$ is asymptotically $c(n)2^{n/2}$, where $c(n)$ takes one constant value for odd $n$ and another for even $n$. This proves Conjecture 1 of Cameron and Erdős, that the count is $O(2^{n/2})$, and with the trivial lower bound $f(n)\ge2^{\lceil n/2\rceil}$ (every subset of the integers in $(n/2,n]$ is sum-free) it gives $f(n)=2^{(1+o(1))n/2}$, the asked exponent, in the sharper form of an asymptotic. The source card green_2004_cameron_erdos_conjecture digests the proof: a family of $2^{o(n)}$ almost sum-free containers, built by Fourier-analytic granularization on $\mathbb Z/p\mathbb Z$, covers every sum-free subset, and a structural step shows that almost every sum-free subset consists of odd numbers or lies in $\{\lceil(n+1)/3\rceil,\ldots,n\}$, whose sum-free subsets Cameron and Erdős had shown to number asymptotically $c(n)2^{n/2}$. The paper notes that the bound $2^{n/2+o(n)}$ was known earlier (Alon; Calkin; Erdős and Granville), so the exponent alone predates it, with its own claim pages Calkin 1990 and Alon 1991; the site's label rests on the full conjecture.

Acceptance. Refereed: the Bulletin of the London Mathematical Society, volume 36, issue 6, pages 769--778, published online 19 October 2004 and in print in November 2004 (Crossref record of DOI 10.1112/S0024609304003650). Reviewed: the site's curator, Thomas Bloom, who is independent of the author, labels the problem PROVED, and his commentary (accessed 2026-09-05 and 2026-10-07, the discussion thread and the proof-claim tab empty at both) credits the bound $f(n)\ll2^{n/2}$ and the two-valued asymptotic to Green and, independently, to Sapozhenko, whose result is the sibling page Sapozhenko 2003. Read depth: Theorem 2 and the introduction were read; the proof was not, and nothing is independently reviewed by this project.

Formalization. Boris Alexeev's lean-proofs repository holds Erdos748.lean, whose header calls the file a Lean formalization of a solution to Problem 748, names Green and Sapozhenko as its informal authors and Codex and GPT-5.6 Sol as its formal authors; the formal-conjectures statement Erdos748.erdos_748 (category research solved, added 2026-09-20) points its formal_proof at it. Its theorem erdos_748 proves the exponent form $\log_2f(n)/n\to1/2$ by a graph-container argument on a cyclic link graph; it does not prove the bound $O(2^{n/2})$ or the two-valued asymptotic of Theorem 2. This corpus has not built or audited that Lean, so it is a formalization link and no formalized evidence is listed.

Date. The page is dated by the arXiv posting of 4 April 2003 (math/0304058, v1, the only version, whose comment field says the paper is to appear in the Bulletin).

Depends on. No page of this wiki.