---

Claim. For the function $f(n)$ of Problem 788 there are absolute constants $c,C>0$ such that, for all sufficiently large $n$,

$$c\sqrt{n\log n}\le f(n)\le n^{\frac12+C\left(\frac{\log\log n}{\log n}\right)^{1/3}},$$

so that $f(n)=n^{1/2+o(1)}$. This answers the problem's particular question yes and gives the order of growth of $f(n)$ up to the $o(1)$ in the exponent, the exponent Choi conjectured in 1971. The claimed result is Theorem 1.1 of S. Wang, A Proposed Solution to Erdős Problem 788, a 15-page manuscript in the author's public repository (the file 788/paper.pdf, PDF metadata dated 22 July 2026, linked above at the repository's commit of 2 August 2026); library home wang_2026_proposed_solution_erdos_problem_788, result page Theorem 1.1. Its Remark 1.2 says the upper bound holds for every large $n$, not only along a subsequence. The manuscript's $f(n)$ is the site's: the open intervals $(n,2n)$ and $(2n,4n)$, sums of distinct elements, and the greatest $t$ such that every $B$ admits an admissible $C$ with $|B|+|C|\ge t$. The route, as the manuscript's plan and the author's claim summary describe it: the identity $f(n)=\min_B(|B|+\alpha(G_B))$ over the sum graph $G_B$ on the inner interval (Proposition 2.1); for the upper bound, $B$ is built over $\mathbb F_p^{2r}$ as the union of the kernels of a family of $p^{o(r)}$ surjective $\mathbb F_p$-linear maps to $\mathbb F_p^r$ that form a strong seeded extractor (Theorem 4.1), so that a $C$ avoiding $B$ has, under each map, an image containing no pair $z,-z$ and so filling at most about half of the target, while the extractor property makes some map spread any large $C$ nearly evenly, a contradiction; the vectors are then identified with base-$p$ integers and the sums produced by carries are added to $B$; the lower bound combines a chromatic-number bound for a graph whose edges use few label sums (Lemma 3.1) with the sparse-neighborhood coloring theorem of Alon, Krivelevich and Sudakov. The author's note on the site's claim tab says the proof was found by the author's AI pipeline using GPT-5.6 Sol, and the manuscript's abstract ends "This proposed solution was found by GPT-5."; the author is named alone.

Submission note. Posted to erdosproblems.com as a proof claim by Shouqiao Wang (account ShouqiaoWang) on 19 July 2026, giving "GPT-5.6 Sol" as the AI used:

We prove the stronger version

$$> c\sqrt{n\log n}\le f(n)\le n^{1/2+O\left((\log\log n/\log n)^{1/3}\right)}, >$$

and hence $f(n)=n^{1/2+o(1)}$. Think of $B$ as a small list of sums that has to catch a pair from every large $C$. Over $\mathbb F_p^{2r}$, we take $B$ to be the union of the kernels of several carefully chosen linear maps. If $C$ avoids $B$, then the image of $C$ under any one of these maps cannot contain both $z$ and $-z$, since the corresponding two elements of $C$ would have a sum in the kernel. Thus every image occupies at most about half the target space. The maps are chosen so that every large $C$ is spread almost evenly by at least one of them, giving a contradiction. We then identify vectors with base-$p$ integers and include the extra sums caused by carries. The lower bound is a separate coloring argument for the associated sum graph. Notes: The proof is found by my AI pipeline using GPT-5.6 Sol. I will provide the lean formalisation of the proof soon!

Depends on. Nothing in this wiki: the argument is the manuscript's own.

Formalization. The same repository's Lake project 788/lean (toolchain leanprover/lean4:v4.27.0, Mathlib at v4.27.0), which the author added to the claim thread in a comment of 23 July 2026, proves theorem erdos788 : MainTheorem in Erdos788/FinalTheorem.lean. Its Definitions.lean defines f n over Finset.Ioo n (2 * n) and Finset.Ioo (2 * n) (4 * n) with distinct summands, which agrees with the site's definition at statement level (open intervals, distinctness, quantifier order), and Statement.lean defines MainTheorem as the manuscript's two bounds, with the lower-bound constant $1/2000$ for every $n\ge3$, together with the site's question in its $\varepsilon$ form. Fifteen of the 43 modules and the root contain no sorry, axiom or native_decide at the pinned commit; that check covers no other module. The repository's workflow rejects those tokens by a text search and builds the project, with one successful run listed (23 July 2026). The corpus has not built the development, so this link is a posting of the claim and not formalized evidence.

Standing. Claimed. No acceptance evidence: the site's label was OPEN on 2026-09-18 and on 2026-10-06, and its commentary, last edited 26 January 2026, predates the claim and does not adopt it; the site's tab warns that a listing there does not guarantee correctness; no arXiv version, journal record, independent review or citing paper was found on 2026-09-18; and the one comment on the claim (still the only one on 2026-10-06) is the author's own, adding the Lean link. The repository's README says each proof was checked with the help of AI, which is the author's own statement. The problem page records the best refereed upper bound, $(n\log n)^{2/3}$, and the site's $n^{3/5+o(1)}$ route; this claim, if accepted, would close the gap between them and the elementary lower bound $n^{1/2}$.