---

Claim. The second question of Problem 367 fails at $k=3$ by more than the $n^2\log n$ rate: for every $M$ there is $n$ with

$$B_2(n)\,B_2(n+1)\,B_2(n+2)>M\,n^2\log n,$$

so the ratio of the product to $n^2\log n$ is unbounded. The construction runs the Pell sequence of van Doorn's claim over a finite set $S$ of primes $p\equiv5\pmod8$ at once: with $\alpha=3+\sqrt8$ one has $\alpha^{p(p+1)/2}\equiv-1\pmod{p^2}$, so for a suitable index $j$ every $p^2$ with $p\in S$ divides $n_j+2$, giving $B_2(n_j+2)\ge\prod_{p\in S}p^2$ while $\log n_j\ll\prod_{p\in S}p(p+1)/2$; the gain $\prod_{p\in S}2p/(p+1)$ tends to infinity with $S$. Hughes posted the result in the problem's thread on 2026-06-10 with a Lean 4 repository, pinned above at its commit of that day, whose README describes it as the formalized results accompanying a paper of Hughes's on powerful parts of consecutive integers and Davenport–Zannier polynomials.

Submission note. Posted to the site's forum by S. D. Hughes on 10 June 2026:

Some progress on this problem and its $B_r$ extension. The main constructions are vibe formalized in Lean 4/Mathlib — zero sorries, standard axioms, the audit prints at build time — here.

1. The $B_r$ extension (in its nontrivial reading — some $\varepsilon(r,k)>0$): resolved affirmatively for all $r,k\ge2$, with any $\varepsilon<\frac{r+1}{r^2}$. For odd $r$: $n=(t^r-1)^r$, so $B_r(n)=n$ and $n+1=t^r\Psi_r(t)$; Schur+Hensel force $s^r\mid\Psi_r(t)$ with $s^r\asymp t$ by taking $t$ in one period. Even $r$: same with $n=(t^r+1)^r-1$.

2. The $k=3$ lower bound strengthens to $\limsup_n \frac{B_2(n)B_2(n+1)B_2(n+2)}{n^2\log n}=\infty$: run the Pell construction with a finite set $S$ of primes $\equiv5\pmod 8$ simultaneously ($\alpha^{(p+1)/2\cdot p}\equiv-1\bmod p^2$, odd quotients), giving $B_2(n_j+2)\ge\prod_{p\in S}p^2$ with $\log n_j\ll\prod_{p\in S}\frac{p+1}2p$; the gain is $\ge\prod_{p\in S}\frac{2p}{p+1}\to\infty$.

3. For two-term cube-full parts, $E_3:=\limsup_n\frac{\log(B_3(n)B_3(n+1))}{\log n}$ satisfies

$$> \tfrac{40}{27}\ \le\ E_3\ \le\ \tfrac32,$$

the upper bound conditional on

$abc$, the lower bound via an explicit degree-27 Davenport–Zannier identity $G^3+N^3=HC^3$ ($N=2^{14}3^4$, $G'=9C^2$) plus the same Hensel device; a rational identity of this shape of degree $3d$ gives $E_3\ge\frac32-\frac1{6d}$, so a family with $d\to\infty$ would pin $E_3=\frac32$ under $abc$.

Also recorded: under $abc$, $\prod_{n\le m<n+k}B_2(m)\ll_{k,\varepsilon}n^{2+\varepsilon}$ for every fixed $k$ (Granville–Langevin radical bound applied to $\prod_{i<k}(x+i)$). The unconditional weak form of course remains open.

Covers. The second question (the part strong_bound), already answered no on van Doorn's page; this claim sharpens the rate at $k=3$ from $\gg n^2\log n$ infinitely often to an unbounded ratio against $n^2\log n$. Not covered: the first question (the part weak_bound), on which Hughes has a separate conditional claim.

Depends on. Nothing in this wiki; the Lean development is self-contained, and van Doorn's page is cited for the construction it extends.

Standing. Claimed. Three things qualify the Lean. First, the repository's headline theorem erdos367 in the module PellLimsup, that for every real $M$ some $n$ has the product above $M\,n^2\log n$, holds trivially at $n=1$, where $n^2\log n=0$ and the product is $1$. Second, the unbounded ratio therefore rests on the lemma erdos367_key, that for every $N$ some index $j\ge1$ has $B_2(n_j+2)>N\log n_j$, together with the lemmas L1 and L2, that $B_2(n_j)=n_j$ and $B_2(n_j+1)=n_j+1$; along $j\ge1$ the lemma does give the claim. Third, the paper the README cites has no public posting. The README reports that every module builds without sorry and that each theorem depends only on propext, Classical.choice and Quot.sound, with no native_decide. The corpus has not built or audited the repository, so no formalized evidence is listed; the site labels the problem OPEN (page last edited 23 March 2026) and its commentary does not mention this result, so no reviewed evidence is listed either. The same repository carries Hughes's other claims: the $B_r$ variant of the site's commentary for odd $r$ (erdos367_iv, with $n=(q^r-1)^r$) and an arithmetic core for Hughes's bounds on $E_3=\limsup\log(B_3(n)B_3(n+1))/\log n$ under explicit prime-supply hypotheses; the problem page records them.