---

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

$$F(n)\asymp\frac{n\log\log n}{\log n}.$$

The lower bound was already known: the primes together with the squarefree semiprimes form such a set, and Landau's count of integers with exactly two prime factors gives it size $(1+o(1))\,n\log\log n/\log n$ (the semiprime construction posted in the thread in August 2025). The new part is the matching upper bound $F(n)\ll n\log\log n/\log n$, Theorem 1.1 of the manuscript "A square-product rigidity problem of Erdős, Sárközy and Sós" (draft dated 24 April 2026, no author named). The argument first reduces to squarefree sets by fixing the square part of each element. A squarefree element with at least two prime factors is written $cpq$ with $p<q$ its two largest prime factors; for dyadic ranges of $p$ and $q$ and a fixed core $c$ the elements $cpq$ form a bipartite graph colored by $c$, and the rigidity condition forbids a $2\times2$ rectangle complete in two colors. A colored Kővári--Sós--Turán supersaturation estimate, with elementary estimates (Chebyshev, Mertens, partial summation) for smooth squarefree cores, bounds the total. This page rests on the manuscript's abstract and introduction only.

Submission note. Posted to the site's forum by Przemek Chojecki on 25 April 2026:

With GPT-5.5 Pro I've got

$$F(n)\asymp \frac{n\log\log n}{\log n}.$$

The lower

bound is supplied by all primes and squarefree semiprimes (as noted in the comments too). The upper bound is the main point. After reducing to squarefree sets, we write each element with at least two prime factors as

$$a=c p q, >$$

where $p<q$ are the two largest prime factors of $a$. For dyadic prime

intervals $p\in(X,2X]$, $q\in(Y,2Y]$, and for each core $c$, the elements $c p q$ form a bipartite graph in the variables $p,q$. The rigidity hypothesis forbids a $2\times2$ rectangle from being complete in two different colors $c,d$. This converts the problem into a weighted colored graph problem. The main term in the graph estimate is exactly of size $n\log\log n/\log n$; the remaining terms are smaller because the core $c$ has all prime factors below the lower graph coordinate.

Here is the note and here is the formalization with Aristotle - the formalization is not complete because of Merten's theorem used as well as couple of other estimates.

Claimant. The manuscript names no author. The forum post of 25 April 2026 by the user Przemek (Chojecki) announces the result as found by GPT-5.5 Pro and links the manuscript and a Lean file; the site's commentary credits the proof to GPT-5.5 Pro prompted by Chojecki. The page is filed under the prompter's surname.

Acceptance. The site's curator, Thomas Bloom, accepted the result, and the curator had no part in it: the problem page is labeled SOLVED (LEAN), its commentary as of 2026-10-07 (last edited 28 May 2026) says the semiprime lower bound is best possible up to constants and credits the upper bound to GPT-5.5 Pro prompted by Chojecki, and the curator's post of 3 May 2026 in the thread compares the argument with Erdős's 1968 method for a weaker form of Problem 425 and calls it a natural generalization in hindsight. This is the reviewed evidence. There is no refereed version. The formal-conjectures catalog tags its statement file research solved and registers the Lean proof below; catalog agreement is noted, not required, and the statement file is not itself a formalization. Nothing is independently reviewed by this project. A later claim sharpens the order to the asymptotic $F(n)\sim n\log\log n/\log n$ (claim page).

Formalization. The Lean file at ulam.ai is the prompter's own and is declared incomplete in the post (Mertens' theorem and some other estimates are left unproved). The catalog registers instead the file src/latest/ErdosProblems/Erdos888.lean of Boris Alexeev's repository plby/lean-proofs at the pinned commit, which declares itself a formalization of this result: its header names Przemek Chojecki and GPT-5.5 Pro as the informal authors and Codex and GPT-5.6 Sol as the formal authors, and its theorem erdos_888 is the catalog's statement (the extremal size is $\Theta(n\log\log n/\log n)$), proved from two imported modules for the lower count and the upper bound. This page rests on the text of the top-level file; nothing was built or audited here, so formalized is not listed and the site's "(Lean)" suffix warrants no kernel credit.

Scope. Full. The question asks for the size of the largest such set, and the order of magnitude is the answer the site records; no asymptotic constant is claimed.