The site's label is PROVED (LEAN): the site records the statement as true and attributes the proof to Szemerédi [Sz76] (J. Number Theory 8 (1976), 264--270). The standing derives from the claim pages: Szemerédi's claim is accepted on the refereed publication and the site's acceptance, and the Erdős--Szemerédi claim is accepted on its refereed publication, so the problem is solved, proved. The paper [Sz76], in the publisher's open archive, states the theorem in its abstract (printed p. 264): "Let $n$ be a positive integer and let $A=\{a_1,\ldots,a_s\}$, $B=\{b_1,\ldots,b_t\}$ be two sets of positive integers such that the product set consists of $st$ distinct numbers. Then, for a certain positive constant $c$, $st\le c\,n^2/\log n$, establishing a conjecture made by P. Erdös", the sets inside $\{1,\ldots,n\}$ by the body's statement of the problem on the same page; the closing line of the proof (p. 269) gives $|A|\cdot|B|<C(n^2/\log n)$ for every $n\ge2$ with $C$ written out in the Brun and Mertens constants. It is the paper Erdős's 1972 attribution announced ("Szemerédi recently found a surprisingly simple proof of (1), his paper will appear in the Journal of Number Theory", printed p. 81), and it calls its own argument "the surprisingly simple proof of (2)". A second proof is Theorem 1 of Erdős and Szemerédi, On multiplicative representations of integers, J. Austral. Math. Soc. Ser. A 21 (1976), 418--427 (refereed; printed p. 421), which proves the statement, $kl<cx^2/\log x$, by "a simpler proof of (4), which nevertheless uses many of the ideas of the original proof", and which the site's discussion thread links. The limit question Erdős asked next, whether $\max|A||B|\log N/N^2$ converges and to what, is open; [Sz76] records only the hope to investigate whether the bound holds "for avery [sic] $c>1$ if $n>n_0(c)$" (p. 265), Erdős and Szemerédi conjectured the value $1$, and a forum construction of 7 September 2026 reports a constant above $1$ (not checked here). The site's label carries the suffix (LEAN); what it refers to is set out under Formalization and the Lean label below, and no local kernel credit is claimed.