---

Claim. Let $p_1<p_2<\cdots$ be the primes, with the convention $p_0=1$, under which $n=1$ lies in $[p_0,p_1)$ and counts; the formal-conjectures statement adopts the same convention. If $p_{k-1}\le n<p_k$ and every prime dividing $n!+1$ is $p_k$ or $p_{k+1}$, then $n\le5$; so $n=1,2,3,4,5$ are the only such $n$, and Problem 1058 is answered affirmatively: there are only finitely many. This is the Theorem of F. Luca, On a conjecture of Erdős and Stewart, Math. Comp. 70 (2001), no. 234, 893–896, received 1999-01-04 and published electronically 2000-03-08, the date this page carries; the source card is luca_2001_conjecture_erdos_stewart. The conjecture it proves is the one Guy reports as Erdős and Stewart's in Problem A2 of Unsolved problems in number theory.

Method. A $2$-adic lower bound for linear forms in two logarithms (Bugeaud–Laurent), applied to $\operatorname{ord}_2(n!)= \operatorname{ord}_2(p_k^ap_{k+1}^b-1)$, gives $n<7\,242\,116$ (so $p_{k+1}<7.5\cdot10^6$); a computer search over cubic residues modulo the primes $q\le193$ with $q\equiv1\pmod 3$ forces $3\mid a$ and $3\mid b$ in any remaining solution, which the Erdős–Obláth theorem on $x^p\pm y^p=n!$ excludes; a second computation disposes of $n\le193$. No independent check of the proof is recorded.

Acceptance. The paper is refereed: Math. Comp. 70 (2001), no. 234. The site's curator, Thomas Bloom, marks Problem 1058 proved and credits Luca's paper. The formal-conjectures statement for Problem 1058 is closed by sorry but carries a formal-proof attribute pointing at the Lean 4 file linked above, which declares itself a formalization of Luca's solution (informal author Florian Luca; formal authors recorded as the AI systems Codex and GPT-5.6 Sol) and proves that $n$ is a solution exactly when $n\in\{1,2,3,4,5\}$. That file is linked as the claimant's formalization; this corpus has not built or audited it, so it is not listed as formalized evidence.

Depends on. No other wiki page; the claim rests on the cited paper.