---

Claim. Alex Chengyu Li's full proof claim asserts that for every $N\ge1$ the maximum size of a set $A\subseteq\{1,\ldots,N\}$ with $ab+1$ never squarefree for $a,b\in A$ is

$$\left\lfloor\frac{N+18}{25}\right\rfloor,$$

which is the number of $n\le N$ with $n\equiv7\pmod{25}$; so the class $7\bmod25$ attains the maximum for every $N$ and the answer to Problem 848 is yes, with no finite range left unchecked. The route the summary describes: the upper bound is restated, through an exact Hall-type matching equivalence, as an inequality between the elements outside the class $C_N$ of residues $7\bmod25$ that are compatible with the condition and their neighbors inside $C_N$ under the squarefree-product relation; for $N\le5\cdot10^6$ a certified family of prefix colorings gives the bound directly; beyond that range, estimates on square divisors together with matching arguments confine any failure of the Hall condition to a residual set of fixed shape, which is sorted by its $2$-adic behavior into five types and by residue modulo $9$; arguments with three and four pivots, and bounds on the number of solutions of a transformed quadratic equation, dispose of each branch; what is left are exact rational inequalities over finitely many structural cases, and a single argument covers every $N\ge5\cdot10^{11}$. The manuscript, on SSRN, and the Lean project were not read.

Submission note. Posted to erdosproblems.com as a proof claim by Alex Chengyu Li (account alexchengyuli) on 16 August 2026, giving "OpenAI ChatGPT 5.5; OpenAI ChatGPT 5.6; and a personally developed AI-assisted research and proof-engineering system." as the AI used:

The upper bound is first reformulated, via an exact Hall equivalence, as a neighbourhood inequality between compatible elements outside $C_N$ and their squarefree-product neighbours inside $C_N$. For $N \le 5\cdot 10^6$, a certified family of prefix colourings establishes the bound directly. Above that range, square-divisor estimates and matching arguments reduce any possible Hall defect to a structured residual. This residual is partitioned according to five $2$-adic types and residue classes modulo $9$. Three- and four-pivot arguments, together with bounds for the number of solutions to a transformed quadratic equation, control every resulting branch. The remaining estimates reduce to exact rational inequalities over finitely many exhaustive structural cases, followed by a uniform argument for (N \ge 5\cdot 10^{11}). These ranges cover every $N$, proving that the maximum is

$$> \left\lfloor\frac{N+18}{25}\right\rfloor$$

for every $N\ge1$. Notes: A

complete source-only rebuild is possible, but it is large and time-consuming. For independent replay, I strongly recommend using the released, hash-bound OLean cache: https://github.com/crabsatellite/erdos-848-squarefree-product/releases/tag/v1.0.5-kernel Check out the exact tag v1.0.5-kernel, download all 75 cache-shard ZIP files together with the manifest and checksum assets, and place them in one directory. Then run: python -B scripts/install_release_cache.py --asset-dir --prepare-dependencies --kernel --memory-mib 32768 The installer verifies the checked-out source commit, pinned Lean toolchain, publication manifest, every downloaded shard, and every decompressed OLean before running the trust-zero kernel gates. Do not run lake update. A machine with approximately 32 GiB of memory and at least 200 GB of free disk space is recommended.

Postings. The result was first made public in the author's GitHub repository as the release v1.0.0-kernel, titled an all-$N$ kernel proof and published 30 July 2026 (its commit is linked above; the repository's release list, has no earlier release), which names this page; it was followed by code archives on 1 August, by the release v1.0.5-kernel of 4 August 2026, whose tag resolves to the commit the Lean link above is pinned to, by a source release the same day and by four manuscript freezes, two on 4 August and two on 6 August 2026. The full proof claim on the site's proof-claim tab was submitted 16 August 2026 with a tools line naming OpenAI ChatGPT 5.5, OpenAI ChatGPT 5.6 and an AI-assisted research and proof-engineering system of the author's own, linking the SSRN manuscript (whose posting date was not confirmed: the record was not readable) and the Lean 4 file of the v1.0.5-kernel release. The claim's notes say that a source-only rebuild is possible but large, and recommend replaying the released, checksum-bound compiled cache (75 shards, about 32 GiB of memory and 200 GB of disk) through the project's installer, which they say verifies the source, toolchain, manifest and every shard before running the kernel checks.

Acceptance. None on record. The site's label is DECIDABLE for the earlier result of Sawhney for all large $N$, its page was last edited 6 December 2025, before the claim, and the curator has not acted on it (proof-claim tab accessed 2026-10-06 and 2026-10-07). The two comments on the claim are forum users' posts. The first, of 19 August 2026, reports its writer's own check of the main steps with code of the writer's own: that the formal statement is the problem as posed (four deliberately wrong variants were shown false), that the value $\lfloor(N+18)/25\rfloor$ holds for every $N\le100{,}006$ by the writer's own search, that the constants of the threshold note recorded on Sothanaphan's page come out the same on recomputation (with a true crossover near $2.636\cdot10^{17}$), and that the middle-range inequalities hold as exact rationals, the tightest by a margin near $10^{-5}$; it adds that the released compiled cache serves one platform only, so that other systems need a source rebuild; and it reports that a second, independent determination of the value for every $N$, published by Ian Pitchford with OpenAI Codex as its reported author and recorded on its own page, agrees with this one. The second comment, of 24 August 2026, only links an external record of the claim. A forum comment is neither a named reviewer nor a referee, so it is not listed as evidence. The formalization is not listed either: nothing was downloaded, built or audited here, and no statement-fidelity review exists in this corpus. The claim stays claimed, and the problem's standing is claimed, proved, through this page and the agreeing full claim of Pitchford.

Depends on. No page of this wiki.