---

Claim. The second question of Problem 367, whether $\prod_{n\le m<n+k}B_2(m)\ll_k n^2$ for every fixed $k\ge1$, has answer no. For $k\le2$ the bound is trivial, since the product is at most $n(n+1)\le2n^2$. For every $k\ge3$ it fails: there is $c>0$ with

$$\prod_{n\le m<n+3}B_2(m)>c\,n^2\log n$$

for infinitely many $n$, and the product over $k\ge3$ consecutive integers is at least the product over the first three. The construction, posted by Wouter van Doorn in the problem's thread on 2025-11-20, takes the solutions $(x_j,y_j)$ of $x^2-8y^2=1$ and $n_j=8y_j^2$, so that $n_j$ and $n_j+1=x_j^2$ are both powerful and $B_2(n_j)B_2(n_j+1)=n_j(n_j+1)$; the point is that $n_j+2=x_j^2+1$ has a large powerful part along a subsequence. Van Doorn posted the congruence that gives it, $5^t\mid n_{j_t}+2$ along indices $j_t$, as an assumption to be checked. Terence Tao, with the assistance of Gemini Deepthink, proved it the same day: with $\alpha=3+\sqrt8$ one has $\alpha^{\pm3}=-1+5(20\pm7\sqrt8)$, by induction $\alpha^{\pm3\cdot5^{t-1}}\equiv-1\pmod{5^t}$ in $\mathbb{Z}[\sqrt8]$, and for $j_t=(3\cdot5^{t-1}-1)/2$ this gives $5^t\mid n_{j_t}+2$. Since $n_{j_t}<x_{j_t}^2=e^{O(5^t)}$, the product at $n_{j_t}$ is at least $n_{j_t}(n_{j_t}+1)5^t\gg n_{j_t}^2\log n_{j_t}$. The first question, the bound $n^{2+o(1)}$, is untouched by this.

Submission note. Posted to the site's forum by Terence Tao on 20 November 2025:

Gemini Deepthink confirms that your argument negatively answers the second version of the problem. One can streamline the argument as follows:

1. Define $n_j = (\alpha^{2j} - 2 + \alpha^{-2j})/4$, where $\alpha = 3 + \sqrt{8}$ (so $\alpha^{-1} = 3 - \sqrt{8}$). Then \begin{align*} n_j &= 8 \times \left[\frac{\alpha^j - \alpha^{-j}}{2\sqrt{8}}\right]^2 \ n_j+1 &= \left[\frac{\alpha^j + \alpha^{-j}}{2}\right]^2 \ n_j+2 &= \frac{\alpha^{2j} + 6 + \alpha^{-2j}}{4} \end{align*} and both expressions in brackets are integers (OEIS A001109 and A001541 respectively). In particular, $n_j$ is a natural number (OEIS A132592), with $n_j, n_j+1$ already $2$-full.
2. Observe the identity $\alpha^{\pm 3} = 99 \pm 35 \sqrt{8} = - 1 + 5 \times (20 \pm 7 \sqrt{8})$. By induction one can show that $\alpha^{\pm 3 \times 5^{t-1}} = -1 + 5^t (a_t \pm b_t \sqrt{8})$ for various integers $a_t,b_t$ and all $t \geq 1$.

Now we set $j_t :=(3 \times 5^{t-1}-1)/2$ (which is an integer) and compute \begin{align*} 4(n_{j_t}+2) &= \alpha^{-1} \alpha^{3 \times 5^{t-1}} + 6 + \alpha \alpha^{-3 \times 5^{t-1}} \ &= (3-\sqrt{8}) (-1 + 5^t (a_t + b_t \sqrt{8})) + 6 + (3+\sqrt{8}) (-1 + 5^t (a_t - b_t \sqrt{8}))\ &= 5^t (6 a_t - 16 b_t) \end{align*} giving the key claim $5^t | n_{j_t}+2$. Thus for $t \geq 2$

$$> \prod_{n_{j_t} \leq m < n_{j_t}+3} B_2(m) \geq n_{j_t} (n_{j_t}+1) 5^t \gg n_{j_t}^2 \log n_{j_t}. >$$

This looks within range of being "vibe formalizable" in Lean, if anyone wants to give it a shot.

Covers. The second question (the part strong_bound), answered no for every $k\ge3$ with the growth rate $n^2\log n$ infinitely often; for $k\le2$ the bound holds trivially. Not covered: the first question (the part weak_bound), which stays open.

Depends on. Nothing in this wiki; the argument is complete in the two thread posts.

Standing. Claimed. The result exists in the thread and in the Lean file below; it has no arXiv posting, no journal record and no independent review other than Tao's completion. The site's commentary credits van Doorn with the failure for all $k\ge3$ and the $n^2\log n$ rate, but the site labels the problem OPEN (page last edited 23 March 2026) and lists no parts, so that credit is not acceptance and no reviewed evidence is listed. Formalization: the file Erdos367.lean in Boris Alexeev's lean-proofs repository, pinned above at the commit of 2025-11-22, declares itself a formalization of this result; its header names van Doorn as the finder of the proof, says that the proof follows Tao's elaboration with the assistance of Gemini Deepthink, and says that Aristotle, from Harmonic, auto-formalized the argument from the LaTeX source and finished the proof against a statement written by hand, the process operated by Alexeev. Its theorem disproof_367 proves that no constant $C$ has $\prod_{n\le m<n+3}B_2(m)\le Cn^2$ for all $n$, the failure of the bound at $k=3$, not the $n^2\log n$ rate. The formal-conjectures statement file, the record link pinned at the commit of 2026-09-22, states the second question as erdos_367.parts.ii with the answer False, tagged research solved, and the variants k_le_two and k_ge_three_lower as solved, all without proof. The corpus has built none of these files, so no formalized evidence is listed. A later repository of Scott Hughes strengthens the rate to an unbounded ratio against $n^2\log n$; that is a separate claim.