---

Claim. Let $A$ be the set of positive integers congruent to $3\cdot2^i\pmod{2^{i+2}}$ for some $i\ge0$, that is, the integers whose largest odd divisor is $3\pmod4$. Then $a+b$ is never a power of two for $a,b\in A$, equal or not, and $A$ has natural density $1/4+1/8+\cdots=1/2>1/3$, so the question of Problem 1136 is answered yes. Müller also proves that $1/2$ is best possible: every set with the property has lower density at most $1/2$. The source is H. Müller, Über ein additiv-zahlentheoretisches Problem von P. Erdős, Mitt. Math. Ges. Hamburg 30 (2011), 75--78 (Zbl 1283.11054), which reports that Erdős asked the question at the 1987 meeting of the Deutsche Mathematiker-Vereinigung in Berlin. The paper's zbMATH review records both results: every set with the property has lower density at most $1/2$, and Müller's set has the property and lower density $1/2$. No online copy of the paper is linked. The page name's date is the publication year, the day being unknown.

Acceptance. Refereed: the paper appeared in the Mitteilungen der Mathematischen Gesellschaft in Hamburg, volume 30 (2011). Reviewed: the site's curator, Thomas Bloom, labels the problem PROVED (LEAN), last edited 20 January 2026, and the commentary credits Müller with the construction, its density $1/2$ and the matching upper bound (the site's page as of 2026-09-05, when the proof-claims tab was empty). A thread post of 22 April 2026 observes that the greedy sequence (each term the least unused integer that makes no power-of-two sum with the earlier terms) is the same set $A$, by an induction over dyadic blocks. This page rests on no review of its own.

Formalization. Two Lean proof files that declare themselves formalizations of Müller's result are linked, neither built or audited here, so neither is counted as formalized; the site's (LEAN) suffix is its catalog label. The file of 21 April 2026 in the repository Woett/Lean-files (516 lines, importing Mathlib; its header names Müller as the informal author and Aristotle from Harmonic as the formal one, and credits as a similar formalization the gist of 19 April 2026, which names no informal author and is recorded on its own claim page) proves main_result: some set with no power-of-two sum has natural density $1/2$ (its counting function divided by $n$ tends to $1/2$), and every such set has upper density at most $1/2$, which strengthens Müller's lower-density bound, together with a more general theorem for any increasing sequence $s$ with $s_{k+1}\le2s_k+2$ (a subset of $\{1,\ldots,n\}$ with more than $(n+s_1)/2$ elements has two members summing to a term of $s$). It prints its axioms with #print axioms three times. The same development, with a header naming Müller as the informal author and Aristotle, Lorenzo Luccioli and Wouter van Doorn as the formal authors, is src/v4.29.1/ErdosProblems/Erdos1136.lean of plby/lean-proofs (690 lines), which the formal-conjectures file ErdosProblems/1136.lean names as its formal proof. That file states erdos_1136, the existence of a set of lower density above $1/3$ with no power-of-two sum, under category research solved with a formal_proof attribute pointing at that development and a sorry body, plus three sorry-bodied variants (the multiples of $3$, Müller's set, the upper bound): a statement file, not a proof, so it is described here and not linked. The two proof files contain no sorry, axiom declaration or native_decide in their text. The site shows a formalized statement for the problem.

Scope. Full. The upper bound $1/2$ and the general theorem of the thread are stronger statements that the question does not ask for.