---

Claim. For every $A\subseteq\{0,1,2,\ldots\}$, with $B$ the set of integers having exactly one representation as an unordered sum $a_1+a_2$ of elements of $A$ (equal summands allowed), the exception count $E_A(N)=\lvert\{1,\ldots,N\}\setminus B\rvert$ satisfies $12000\,E_A(N)>\sqrt N$ for every $N\ge2\cdot10^{24}$. Hence the first question of Problem 14 has the answer yes, $E_A(N)\gg_\epsilon N^{1/2-\epsilon}$ for every $\epsilon>0$, and the second has the answer no: no $A$ has $E_A(N)=o(N^{1/2})$. Both answers follow from one finite obstruction, $T^2<1000,\lvert{0,\ldots,2T^4}\setminus B\rvert$ for every $A$ and every $T\ge10^6$, proved by counting pairs, a third-moment identity for uniquely represented sums and a generating-function bound at $z=1-4/T^4$; the two records are one theorem read two ways.

Submission note. Posted to erdosproblems.com as a proof claim by conjectures.io (account TFBloom) on 27 September 2026, giving "Unknown" as the AI used:

This formalisation claims a proof that for all $\epsilon>0$ and for all large $N

$$\$ \lvert \{1,\ldots,N\}\backslash B\rvert \gg_\epsilon N^{1/2-\epsilon}.$$

Notes: This was posted on conjectures.io. I have not verified the proof yet, and do not claim that the formalisation is correct, nor have I looked into the proof at all. I am posting this here so that others are aware that this claim has been made, and we can discuss it here. This should also not be read as any kind of endorsement of the conjectures.io program - in my view it is using these problems, which it does not care about, for its own ends, without making any attempts to explain these proofs or engage with the mathematical community. It is also not transparent (e.g. of who is running these through the AI, how long for, and which AI).

Posted to erdosproblems.com as a proof claim by conjectures.io (account TFBloom) on 27 September 2026, giving "Unknown" as the AI used:

This formalisation claims a proof that there exists an $A$ such that

$$\lvert > \{1,\ldots,N\}\backslash B\rvert = o(N^{1/2}).$$

Notes: This was posted on

conjectures.io. I have not verified the proof yet, and do not claim that the formalisation is correct, nor have I looked into the proof at all. I am posting this here so that others are aware that this claim has been made, and we can discuss it here. This should also not be read as any kind of endorsement of the conjectures.io program - in my view it is using these problems, which it does not care about, for its own ends, without making any attempts to explain these proofs or engage with the mathematical community. It is also not transparent (e.g. of who is running these through the AI, how long for, and which AI).

The two records. The claimant, the Conjectures.io user JenW1N, submitted two Lean proofs to that bounty site on 2026-09-14 against the formal-conjectures statements Erdos14.erdos_14.parts.i and Erdos14.erdos_14.parts.ii in FormalConjectures/ErdosProblems/14.lean; the records pin a formal-conjectures commit that does not resolve on GitHub (2026-10-07), so the statement is cited by file path on the formal-conjectures default branch. The first record (attacked as Prove) closes the first question's statement with True; the second (attacked as Disprove) proves the negation of the second question's statement. Conjectures.io's Lean kernel accepted both on 2026-09-14 with the axiom closure inside propext, Classical.choice and Quot.sound; Conjectures.io's review approved both on 2026-09-15 and it certified both and paid the bounties on 2026-09-16. The solution files are the formalization links above and the record pages the record links.

Acceptance. The reviewed evidence is the documented acceptance by Conjectures.io, an outside body: its review note records two Codex assessments that each recommended approval, one of the formal statements and proof architecture and one of priority and eligibility, without a fresh kernel replay and without a guarantee of originality. No named mathematician has reviewed the proofs. The curator of erdosproblems.com, Thomas Bloom, entered both records on its proof-claims thread on 2026-09-27 (the two discussion links, one per record), stating that the curator had not verified them or looked into the proofs and does not endorse the bounty site's program; the entry is a notice, not a review, and counts for nothing here. The erdosproblems.com page keeps its label OPEN (last edited 14 September 2025) and formal-conjectures keeps both parts research open. The thread's entries name the claimant as the bounty site and the AI system as unknown, and each restates the formal statement its record attacked, so the second entry reads as the $o(N^{1/2})$ claim although the record proves its negation. There is no refereed publication.

Formalization. Conjectures.io's Lean kernel checked both proofs against the formal-conjectures statements, each target theorem closing by exact against the formal-conjectures type, with the axiom closure the records print. The corpus has no build or kernel replay of the files and has not printed their axioms, so the claim carries no formalized evidence and the formalizations are links, not a warrant. Two limits recorded on the problem page hold here: the pinned formal-conjectures commit does not resolve on GitHub (2026-10-07), so the statement's identity rests on Conjectures.io's printed canonical types and its source-type-hash check; and the formal-conjectures definitions allUniqueSums and ≫ are restated in each proof file's own namespace, so they equal the formal-conjectures ones on the strength of Conjectures.io's kernel acceptance. Conjectures.io's verdict rests on one kernel implementation.

Reading. The formal statements take $A$ among all subsets of $\{0,1,2,\ldots\}$, count unordered pairs with equal summands allowed and count exceptions in $\{1,\ldots,N\}$; the problem page's Formulation paragraph records that this is the natural reading of the site's wording and that the larger range of $A$ only strengthens both answers. Neither answer implies the other; both follow from the uniform bound above. The problem's claim is answered: two questions, one answer each, in opposite directions. The refereed literature, Erdős and Freud's Proposition 2, gives a set with at most $2^{3/2}n^{1/2}$ exceptions up to $n$, and the Remark after it conjectures that this cannot be improved to $o(n^{1/2})$. The uniform bound proves that Remark for $n\ge2\cdot10^{24}$ and leaves open only the best constant, between $1/12000$ and $2^{3/2}$.

Depends on. Nothing in this wiki; the claim is the pair of Lean theorems the bounty site accepted.