---

Stewart proves that for fixed integers $a>b>0$ there is a threshold, depending only on the number of distinct prime factors of $ab$, beyond which

$$P(a^n-b^n)>n\exp\!\left(\frac{\log n}{104\log\log n}\right),$$

where $P(m)$ is the greatest prime factor of $m$. With $a=2$ and $b=1$ the quotient $P(2^n-1)/n$ exceeds $\exp(\log n/(104\log\log n))$ for every sufficiently large $n$, and that factor tends to infinity, so the limit the problem asks for holds along all integers, not only along a subsequence. The bound is the direct integer specialization, equation (1.8) of the published paper, of the main theorem on Lucas and Lehmer cyclotomic factors; the statement, the edition mapping and the proof locations are on the result page Theorem 1.1 of the source card Stewart 2013. The proof compares a lower bound for the cyclotomic value with upper bounds for its prime-power contributions through estimates for complex and $p$-adic linear forms in logarithms; it is not reconstructed in this repository.

Acceptance. Refereed: C. L. Stewart, On divisors of Lucas and Lehmer numbers, Acta Mathematica 211 (2013), 291--314, first posted as arXiv:1008.1274 on 2010-08-06. Reviewed: the site's curator, Thomas F. Bloom, records the problem as proved in the affirmative by this theorem on the problem page (last edited 2026-02-01). The problem page Problem 977 records Schinzel's 1962 bound $P(2^n-1)>2n$ for $n>12$, which holds for all large $n$, and the restricted-exponent result of Stewart's 1975 paper (its claim page), neither of which settles the problem, and the separate open question about $n!+1$.

Depends on. No page of this wiki.

Formalization. A third party formalized the statement: Erdos977.erdos_977 in src/latest/ErdosProblems/Erdos977.lean of Boris Alexeev's repository https://github.com/plby/lean-proofs, pinned above at the commit the formal-conjectures catalog cites (the file was added on 2026-08-20). The file's header declares it a Lean formalization of a solution to Problem 977, names C. L. Stewart as the informal author and Codex and GPT-5.6 Sol as the formal authors, and cites Stewart's formula (1.8) and Yamada's 2006 note on the divisibility of Fermat quotients as its mathematical sources. Its unconditional proof of the limit follows the alternative route that Stewart's paper itself records (arXiv:1008.1274v1, displays (10)-(11), pp. 4-5): a uniform bound $\mathrm{ord}_p(2^{p-1}-1)\ll p/(\log p)^2$ of the shape T. Yamada proved (J. Number Theory 130 (2010), 1889-1897; arXiv:math/0607072, the paper the file's header cites under another title), proved in the file by a $p$-adic interpolation determinant and used through a cyclotomic reduction in place of Stewart's Lemma 8. Stewart's estimate (1.8) enters only as the hypothesis of the separate transfer theorem erdos_977_of_stewart. The file therefore checks, in qualitative form, the alternative proof the paper sketches, not the proof of (1.8). The file prints the theorem's axioms. This corpus has not built the file or audited its definitions, so the claim carries no formalized evidence and the evidence stays reviewed and refereed.