---

Claim. Let $F(n)$ be the largest size of a set $A\subseteq\{1,\ldots,n\}$ such that $ad=bc$ whenever $a\le b\le c\le d$ lie in $A$ and $abcd$ is a square. Then, as $n\to\infty$,

$$F(n)\sim\frac{n\log\log n}{\log n},$$

so the leading constant of the accepted order of magnitude is one. Theorem 1.1 of the note The leading constant in Erdős Problem 888 (draft dated 16 September 2026, no author line) proves the equivalent statement $0\le F(n)-Q_2(n)=o(n\log\log n/\log n)$, where $Q_2(n)$ counts the squarefree semiprimes up to $n$, whose Landau asymptotic gives the lower bound. The upper half keeps the square-part reduction and the two-largest-prime encoding $a=k^2cpq$ of the earlier proof and truncates its parameters: elements with $k>K$ or $c>2^L$ contribute at most a fraction of the main term that vanishes as $K$ and then $L$ grow, by the earlier colored-graph estimates; for each of the finitely many remaining multipliers $b=k^2c$ the retained pairs $\{p,q\}$ form a graph $H_b$ on the primes, the union of these graphs has at most $Q_2(n)$ edges, and any two of them intersect in a graph without four-cycles, which has $O(n/\log n)$ edges. This page rests on the note's abstract, introduction and closing sections.

Submission note. Posted to erdosproblems.com as a proof claim by Rogerhu (account Rogerhu) on 17 September 2026, giving "GPT-6 Astra" as the AI used:

We prove $F(n)\sim h(n):=n\log\log n/\log n$. Using estimates from the earlier proof, restricting the representation $a=k^2cpq$ to $k\le K$ and $c\le2^L$ discards at most

$$> \left(\frac{C_1}{K}+C_2K\eta(L)\right)h(n)+o_{K,L}(h(n)), \qquad > \eta(L)\to0\quad(L\to\infty).$$

There are only finitely many possible

remaining $b=k^2c$, independently of $n$. For each $b$, let $H_b$ contain the edge $\{p,q\}$ for each retained representation $a=bpq$. The union of their edge sets has size at most $Q_2(n)$, the number of squarefree semiprimes up to $n$. For $b_1\ne b_2$, the intersections (H_{b_1}\cap H_{b_2}) are $C_4$-free, so the total overcount is $O_{K,L}(n/\log n)$. Letting $n\to\infty$, then $L\to\infty$, and finally $K\to\infty$, and using the existing matching lower bound, gives the asymptotic. Notes: The proof of the leading-constant refinement was found by GPT-6 Astra. The writeup and Lean formalization were developed using OpenAI Codex. The summary was prepared from my Chinese draft with AI-assisted translation and editing.

Depends on. The order-of-magnitude proof on the accepted Chojecki claim page, whose squarefree bound and colored block estimate the note takes as inputs.

Claimant. The note names no author; it credits the proof of the sharp asymptotic to GPT-6 Astra and the exposition and Lean formalization to OpenAI Codex, as the site's proof-claim entry also states. The repository Rogerhu12/erdos888-sharp on GitHub is the publication, released as v0.1.0 on 16 September 2026 and submitted to the site's proof-claim form by the user Rogerhu on 17 September 2026; the page is filed under the forum username Rogerhu, who submitted the claim and publishes the repository Rogerhu12/erdos888-sharp.

Standing. No reply, review or acceptance appears on the site as of 2026-10-07: the thread carries no post after May 2026 and the commentary (last edited 28 May 2026) records the order of magnitude only, so the claim stays claimed. The order itself is settled on the accepted Chojecki claim page; the accepted standing of the problem does not rest on this page.

Formalization. The repository's Lean development, at the pinned commit, proves sqProdRigid_sharp_asymptotic and sqProdRigid_ratio_tendsto_one in formal/Erdos888Sharp/Main.lean, importing the completed order-of-magnitude proof and analytic lemmas from 73 unchanged modules of Boris Alexeev's repository plby/lean-proofs and keeping the definitions of the Lean file supplied with the earlier solution. The note records an audit of twelve statements with the axioms propext, Classical.choice and Quot.sound only, and a fresh-environment build; this page rests on the text of the main file, and nothing was built or audited here, so formalized is not listed, and the statement's fidelity to the problem is not established by this corpus.