---

Claim. For every $k\ge4$ there is a constant $c_k>0$ such that $F_k(N)\le(1-c_k+o(1))N$ as $N\to\infty$, where $F_k(N)$ is the largest size of a subset of $\{1,\ldots,N\}$ with no $k$ distinct elements whose product is a square. In particular $F_5(N)$ is not $(1-o(1))N$, and neither is $F_{2k+1}(N)$ for any $k\ge2$, so both of the site's questions are answered no. This is Theorem 1.2 (Main theorem) of T. Tao, On product representations of squares, arXiv:2405.11610 (v1, 19 May 2024; v3, 23 October 2024), Acta Math. Hungar. 175 (2025), no. 1, 142--157, DOI 10.1007/s10474-025-01505-7; the source card digests it. The proof is a probabilistic double-counting argument using Mertens' theorems and the prime number theorem, and the parity of $k$ plays no role in it.

Acceptance. Refereed: the paper appeared in Acta Mathematica Hungarica, volume 175 (2025); the arXiv comment of v3 calls it the final version incorporating referee comments. Reviewed: Thomas Bloom, the site's curator, independent of the claimant, labels the problem DISPROVED (LEAN), last edited 17 October 2025, and the commentary attributes the negative answer to Tao with the bound above; the discussion thread and the proof-claim tab carried no post as of 5 September 2026.

Formalization. One Lean file is linked: Erdos121.lean of Boris Alexeev's collection lean-proofs at the pinned commit, in the collection since 17 August 2026, which describes itself as a Lean formalization of a solution to the problem, names Terence Tao as the informal author and Codex and GPT-5.6 Sol as the formal authors, and proves, for every $k\ge4$, a constant $c>0$ with the extremal size at most $(1-c)N$ for all large $N$. The site's DISPROVED (LEAN) page thanks Boris Alexeev. This corpus did not build or audit the file, so it is linked and not counted as formalized; the evidence stays reviewed and refereed. The formal-conjectures statement of the problem, added on 22 September 2026 with a formal_proof attribute pointing at this file, is described on the problem page; a statement file is not a formalization and is not linked here. The community database lists the problem's formal status as Lean and has no field for a formal proof's location.

Scope. Full. The function $F(N)$ of the commentary, the largest size of a subset with no odd number of elements multiplying to a square, is a different question with its own asymptotic and is not part of this claim.