Growth of $F(n)$, the largest prime factor of $n(n+1)$: how small can it be? (Erdős #368)

For a positive integer $n$ let $F(n)$ denote the largest prime factor of $n(n+1)$. The problem is to determine the order of growth of $F(n)$ — in particular how small $F(n)$ can be infinitely often. Erdős conjectured that $F(n)\gg (\log n)^2$ for all $n$, and moreover that for every $\epsilon>0$ there are infinitely many $n$ with $$F(n) < (\log n)^{2+\epsilon}.$$ Establish lower bounds for $F(n)$ valid for all $n$, and/or construct infinite families of $n$ making $F(n)$ as small as possible.

Acceptance. FULLY RESOLVES: a complete proof (Lean/Coq machine-checkable preferred, else a full written proof) of Erdős's conjectured lower bound $F(n)\gg(\log n)^2$ for all sufficiently large $n$, and/or a proof that for every $\epsilon>0$ there are infinitely many $n$ with $F(n)<(\log n)^{2+\epsilon}$. Because 'infinitely many' cannot be settled by finite computation alone, a purely numerical submission cannot FULLY RESOLVE the second part. ADVANCES (each independently checkable): a strictly better unconditional lower bound on $F(n)$ than the best stated in the background (currently $\gg (\log\log n)^2/\log\log\log n$), with proof; OR an unconditional construction of an infinite family of $n$ with $F(n)$ smaller, relative to a power of $\log n$, than any previously exhibited, with proof; OR a large reproducible extension of OEIS A074399 identifying record-small values of $F(n)$ (relative to $(\log n)^2$) together with the factorisation code and certificates. Deliver the proof file, the explicit family with proof, or the computation code plus the extended table and record witnesses.