---

Claim. For $n=4$ and for every $n\geq 6$ there are infinitely many collections of $n$ pairwise disjoint intervals $I_1,\dots,I_n$ of integers, each of exactly four consecutive integers, such that the product of all their members is a square. Any one of these infinite families answers the question of Problem 363 in the negative: the collections with every $\lvert I_i\rvert\geq 4$ and square product are not finite in number. The result is the theorem of Maciej Ulas, On products of disjoint blocks of consecutive integers, Enseign. Math. (2) 51 (2005), 331--334. The journal's record gives only the year, so the page is dated by the year's first day; the link is the journal volume's record. Ulas conjectured there that, for each fixed block size, the collections of $n$ blocks with square product are infinite in number once $n$ is large enough.

The family in the formalization. With $f(x)=(x+1)(x+2)(x+3)(x+4)$, one of the parametrizations in the paper, as Wouter van Doorn quoted it on the site's thread, is

$$y^2 = f(4n-1)\,f(4n+3)\,f(4n^2+7n-1)\,f(8n^2+14n+1)$$

with $y=16n(n+1)(2n+1)(2n+3)(4n+1)(4n+3)(4n+5)(4n+7)(4n^2+7n+1)(4n^2+7n+2)$, an infinite family of four disjoint blocks of four whose product is a square.

Acceptance. The result appeared in a refereed journal in 2005, the refereed evidence. The site's curator, Thomas Bloom, writes in the problem's commentary that the statement is false and credits Ulas's theorem: that curator credit is the reviewed evidence. Bauer and Bennett's 2007 paper (card) cites Ulas's theorem for $n=4$ and $n\geq 6$ and settles the cases he left; it does not re-prove his. The remaining cases $n=3$ and $n=5$ with blocks of four are Bauer and Bennett's result, and blocks of five are Bennett and Van Luijk's.

Formalization. The site's "(LEAN)" suffix refers to a Lean 4 file that Wouter van Doorn (forum name Woett) posted on the site's thread on 2026-03-10, obtained with the system Aristotle from Harmonic, which proves that the family above gives infinitely many counterexamples; its header declares itself a formalization of Ulas's result. Boris Alexeev's repository holds a copy with the same declaration, informal author Ulas and formal authors Aristotle and van Doorn, which the formal-conjectures statement file names as the formal proof of erdos_363. Their theorem leaves the number of intervals free, and its validity predicate does not exclude an interval containing $0$, so the statement alone is weaker than the question; the substance is the proof that the family above consists of valid collections of positive integers. The corpus has not built or audited either file, so the page lists no formalized evidence.