---

Shouqiao Wang, A Proposed Complete Solution to Erdős Problem 1038, a preprint in the author's repository (folder 1038), filed on the site's proof-claims tab on 14 July 2026, claims both extremal values. For $f$ in the class of nonconstant monic real polynomials with all zeros in $[-1,1]$ and $E_f=\{x\in\mathbb R:|f(x)|<1\}$, Theorem 1.1 states that an explicit one-variable function $\Lambda$ has a unique minimizer $q_*$ on an interval $(0,q_s]$ and that $\inf|E_f|=L=\Lambda(q_*)$, with certified enclosures $1.834430475762661<L<1.834430475762662$ and $0.025715536866527<q_*<0.025715536866528$; every finite polynomial has $|E_f|>L$, so the infimum is not attained, and $\sup|E_f|=2\sqrt2$ is attained exactly by $(x^2-1)^m$ for $m\ge1$, the supremum being imported from Terence Tao's note on the problem. The lower bound collapses the roots in each component of $E_f$ to their barycenter, following the reduction in Tao's note and in Erdős, Herzog and Piranian, and then compares every finite atomized configuration with a limiting distribution of constant logarithmic potential on its continuous support through a mean-deficit estimate, a convex constant-platform comparison, an endpoint-corrected adjoint identity and a circle rearrangement theorem; the remaining scalar signs are certified by outward interval arithmetic in a companion Python file, and a positive-platform approximation gives polynomials approaching $L$. The paper's library card is wang_2026_proposed_complete_solution_erdos_problem_1038; no independent check of the proofs is recorded.

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

The claimed infimum is $L = 1.834430\ldots$. It comes from a limiting root distribution in which some mass sits at $-1$, while the rest fills one interval so that the logarithmic potential is flat there. The hard part is proving that no polynomial with many separated root clusters can do better. Roots lying in the same component of $\{|f|<1\}$ are first collapsed to their barycenter, which can only shrink the set. The remaining clusters are compared with the flat limiting distribution. Its flatness allows an adjoint identity to split the change in length into a cost for each cluster. After mapping the interval to a circle, rearrangement and Fourier expansion show that every cost is positive. Then we have finite polynomials lie above $L$, while discretizations of the limiting distribution approach it. The supremum $2\sqrt{2}$ follows from Tao's argument.

Depends on. Tao's note for the supremum: Theorem 10.1 applies Theorem 2.1 of the updated note of 27 December 2025 to the root measure of $f$ and proves nothing new there. The infimum rests on the paper's own argument.

Standing. The tab names GPT-5.6 Sol, the paper says that the proposed solution was found by GPT-5.6, and a comment by the author on the claim, of 17 July 2026, adds that it was found through the author's own pipeline and checked by GPT-5.6 Pro and GPT-5.5 Pro. The first comment on the claim, of 14 July 2026, objected that the manuscript's citations were insufficient, that its Section 2 repeated material from Tao's updated note of December 2025 and that its Section 10 copied that note, and asked for an AI disclosure; the author answered on 17 July that the citations were updated and that the manuscript now separates Tao's reductions and one-cut candidate from its own contribution, the lower bound for arbitrary finite root configurations. The site's label is unchanged (OPEN; page last edited 11 January 2026), no reviewer is named and nothing is refereed, so the claim stays claimed. Two independent claims of the same infimum are the page of Darvas, Peng and Tao and Budala's page.

Formalization. On 19 July 2026 the author posted a Lean 4 project in the same folder (toolchain v4.27.0). Its Statement.lean defines a proposition MainTheorem listing every assertion of the main theorem, including the enclosures of $q_*$ and $L$, the two extremal values and the equality cases, and its CompleteProof.lean proves mainTheorem : MainTheorem from two finite numerical tables; an audit file rejects any project declaration depending on sorry, on native evaluation or on the compiler. The corpus has built and audited nothing, so the claim lists no formalized evidence.