---

Claim. Let $(r_i)$ be a periodic sequence of non-zero integers, let $L_n=\mathrm{lcm}(1,\ldots,n)$ and define $X_n$ by $X_n/L_n=\sum_{i\le n}r_i/i$. The note's Corollary states that $\limsup_{n\to\infty}\gcd(X_n,L_n)=\infty$, so in particular $\gcd(X_n,L_n)>1$ for infinitely many $n$. It rests on the note's Theorem: for any bounded sequence of non-zero integers $(r_i)$ and any integer $m$ larger than every $|r_i|$, some $n=e^{O(m)}$ has $X_n$ divisible by a prime larger than $m$; for periodic $(r_i)$ with period $t$, a prime $p>\max(|r_1|,\ldots,|r_t|,t)$ dividing $X_n$ also divides $X_{n'}$ for $n'=np^{\varphi(t)}$, which gives the Corollary. The constant sequence $r_i=1$ gives $X_n=a_n$ in the notation of Problem 291, so the Corollary contains the second question of the problem, that $(a_n,L_n)>1$ for infinitely many $n$, and strengthens it to unbounded common factors. The Lean 4 file linked above, ErdosProblem291.lean, proves the Theorem as ohyeah1 and the Corollary as generalErdos291 over Mathlib without sorry, taking as hypotheses two known results that it does not prove: $m^{2z(m)}<e^{2.52m}$ for all $m\ge4$, with $z(m)$ the number of primes below $m$, which is the Rosser--Schoenfeld bound $\pi(m)\log m<1.26m$ in another form, and $L_n>2^n$ for all $n\ge100$, which follows from Nair's lower bound for $\mathrm{lcm}(1,\ldots,n)$; the file's header says these are expected to follow from a separate prime-number-theorem formalization project. The comment adds that without periodicity the Corollary fails: signs $r_i\in\{-1,1\}$ can be chosen so that $\gcd(X_n,L_n)=1$ for all $n$.

Covers. The second question, that $(a_n,L_n)>1$ occurs for infinitely many $n$, as the case $r\equiv1$ of a statement about every periodic sequence of non-zero numerators, together with the unboundedness of the common factor. Not covered: the first question, whether $(a_n,L_n)=1$ occurs for infinitely many $n$, on which the note and the file say nothing.

Depends on. Van Doorn's 2024 paper is the source the note builds on, by its own account; the two hypotheses of the Lean proof are classical theorems outside the file.

Standing. Claimed. The note, "Generalized harmonic sums have arbitrarily large prime factors", is a PDF in the author's GitHub repository Woett/Miscellaneous, uploaded 5 February 2026 and linked above at its last change; it has no arXiv or journal record. The author announced it and the Lean file in the problem's discussion thread on 6 February 2026, crediting the formalization to Aristotle, Harmonic's automated proving system; the comment is not on the site's proof-claim tab, which is empty, and the site's label is OPEN (as of 2026-10-07; page last edited 12 January 2026), so no curator, referee or named mathematician has accepted the result. The Lean file is third-party Lean that this corpus has not built or audited, and its proof is conditional on the two hypotheses above, so formalized is not listed; the mathematical claim itself is unconditional, since both hypotheses are proved theorems, and the claim is recorded as partial rather than conditional for that reason. The same answer to the second question has two earlier pages, Shiu's criterion and infinitude theorem and Steinerberger's base-3 observation, by different routes.