---

Claim. For $n\ge2$ let $K(n)$ be the least base $k\ge2$ with $\gcd(k^n-1,2^n-1)=1$ and $H(n)$ the least $b\ge3$ admitting a partner $2\le a<b$ with $\gcd(a^n-1,b^n-1)=1$. The manuscript Coprime Power Differences proves, with one absolute constant $C$,

$$\log K(n)\le C\,\tau(n)\,(\log(n+2))^2\qquad(n\ge2),$$

where $\tau(n)$ counts the positive divisors of $n$, and deduces from the elementary maximal order of $\tau$ that for every $\epsilon>0$ and all sufficiently large $n$

$$H(n)\le K(n)<\exp\!\left(n^{(\log2+\epsilon)/\log\log n}\right).$$

The proof is a finite sieve: the primes that must divide an admissible base are separated from the sparse forbidden residue classes, the total density of those classes is bounded through the divisor function, and a truncated inclusion-exclusion finds a base avoiding all of them. The library card covers the manuscript; its pages state the results and sketch the arguments (Theorem 1.1, Lemma 3.1, Corollary 1.2).

Submission note. Posted to erdosproblems.com as a proof claim by Liam Price (account Leeham) on 16 July 2026, giving "GPT 5.6 Sol Pro and Claude Fable 5" as the AI used:

GPT 5.6 Sol Pro proves $H(n)\le K(n)<\exp\bigl(n^{(\log 2+\varepsilon)/\log\log n}\bigr)$ for every $\varepsilon>0$ and all sufficiently large $n$, answering the upper-bound question affirmatively. The Lean formalisation was performed by Claude Fable 5. Notes: I attempted to use a URL shortening service for the Lean, however the link was far too large for it to work. Find the Lean in the comment below.

Covers. Question 3 of Problem 820, yes: $K(n)<\exp(n^{(\log2+\epsilon)/\log\log n})$ for every $\epsilon>0$ and all large $n$, and with it the eventual upper half of question 2, since $H(n)\le K(n)$. The corpus's corollary of Fan and Pollack's Theorem 1.1, through Erdős's Fermat argument, gives the infinitely-often lower bound $H(n)>\exp(n^{0.6736\log2/\log\log n})$. With that bound, the claim answers question 2 yes: the limit superior $c_H$ lies in $[0.6736\log2,\log2]$ and serves as the constant. That combination is the library's growth-constant page, not a statement of the manuscript. Not covered: whether $H(n)=3$ infinitely often; the value of $c_H$; and whether the constant for $K(n)$ equals $c_H$.

Depends on.

• Fan and Pollack's Theorem 1.1, corollary for H(n), for the lower half of the question-2 reading
• the growth-constant page, for the limit-superior combination

The manuscript's own upper bound depends on no page of this wiki.

Claimant. The manuscript's author line reads GPT 5.6 Sol Pro and it carries no date or version number. Liam Price shared it in a partial proof claim on the site's thread on 16 July 2026, crediting the mathematics to GPT 5.6 Sol Pro and a Lean formalization to Claude Fable 5; the page is filed under the submitter's surname. A comment of 17 July 2026 in the thread reports that another run of the same family of systems suggested the same bound; it is not a review.

Standing. No reply by the site's curator, no review and no publication appear as of 2026-10-07: the site labels the problem OPEN and its commentary (last edited 2 December 2025) records only the lower bounds, so the claim stays claimed. The library card's sketches of the argument are this project's own reading and warrant no acceptance.

Formalization. Price's comment of 16 July 2026 in the thread (the third link) carries a Lean playground link selecting the project mathlib-v4.28.0. That URL encodes the whole Lean file, too long for the claim form, so it is not listed in links and is reached through the third link. Its decoded file declares itself a single-file formalization of the manuscript, built against Lean 4.28.0 and Mathlib v4.28.0 and free of sorry, and names the eventual theorems K_lt_exp, H_le_K_and_K_lt_exp and H_lt_exp with the displayed exponent $\log2+\epsilon$, under the positive-base convention for $n\ge2$; its uniform bound states a numerical constant $500$. The file was neither built nor audited here, so formalized is not listed, and the file's own build assertion and the constant $500$ are the source's claims.