---

Claim. With $h(n)$ and $P(n)$ as on the page of Problem 770 and $S(n)=\lfloor\sqrt{4n}\rfloor+1$, Jeffrey Zeng's partial proof claim, submitted to the site's proof-claim tab on 24 July 2026 and made, the listing says, using an OpenAI internal model, asserts for every $n\ge2$ that

$$P(n)\le h(n)\le\max\{P(n),S(n)\},$$

so $P(n)>2\sqrt n$ forces $h(n)=P(n)$, and odd $n$ satisfy $h(n)\le S(n)$. Its sharper criterion: if $p=P(n)>2$ and the number $C(p)$ of ordered coprime pairs in $\{1,\ldots,p\}^2$ exceeds $n$, then $h(n)=p$. The listing's Notes carry the whole ordinary argument: a prime $q$ dividing every $a^n-1$ for $2\le a\le M$ exceeds $M$ and puts $1,\ldots,M$ into the $n$-torsion subgroup of $\mathbf F_q^*$, of order at most $n$; when $q>M^2$ the reduced fractions with numerator and denominator at most $M$ stay distinct in that subgroup, which has too few elements once $M\ge S(n)$ or $C(M)>n$; when $q\le M^2$, a signed pigeonhole representation (for even $n$) or the least quadratic nonresidue bound (for odd $n$) rules $q$ out. The listing says the restriction is needed, since $n=86$ has $P(n)=3$ and $h(n)=5$, and calls the result partial, with novelty and priority undetermined. The library's source card records the listing, and its result page reconstructs the proof with its five elementary lemmas, author-recorded.

Submission note. Posted to erdosproblems.com as a proof claim by Jeffrey Zeng (account jeffzeng) on 24 July 2026, giving "an OpenAI internal model" as the AI used:

AI-assisted, Lean-formalized partial result for #770. Use the collective-gcd, strict-$M>2$ definition of $h(n)$. Let (P(n)=\max{p\text{ prime}:p-1\mid n}) and $S(n)=\lfloor\sqrt{4n}\rfloor+1$. For every positive $n$,

$$> P(n)\le h(n)\le\max\{P(n),S(n)\},\qquad P(n)>2\sqrt n\Rightarrow h(n)=P(n). >$$

If $n$ is odd, $h(n)\le S(n)$. More sharply, if $p=P(n)>2$ and

$C(p)=\#\{(a,b):1\le a,b\le p,\gcd(a,b)=1\}>n$, then $h(n)=p$, including cases with $p\le2\sqrt n$. These are partial results: the density, liminf, and general $\varepsilon>0$ questions remain unresolved. Novelty and priority have not been determined. AI disclosure: an OpenAI internal model. Notes: Put $G(n,M)=\gcd_{2\le a\le M}(a^n-1)$. If $q\mid G(n,M)$, then $q>M$, and $H=\{x\in\mathbf F_q^*:x^n=1\}$ has at most $n$ elements. For $q>M^2$, reduced fractions $a/b$, $1\le a,b\le M$, inject into $H$. Their count is $C(M)\ge M^2/4+M$, so $M\ge S(n)$ or $C(M)>n$ gives a contradiction. For $q\le M^2$ and even $n$, Dirichlet gives $x=a/k$ with $1\le k\le M$ and $0<|a|<M$, so every $x\ne0$ satisfies $x^n=1$; hence $q-1\mid n$, contradicting $q>P(n)$. For odd $n$, all elements of $H$ are squares and the least quadratic nonresidue is at most (\lceil\sqrt q\rceil), forcing $q>M^2$. Fermat gives $P(n)\le h(n)$. The restriction is necessary: $n=86$ has $P(n)=3$ but $h(n)=5$.

Covers. The third question for every fixed $\epsilon>1/2$: since $n^\epsilon>2\sqrt n$ for large $n$, $P(n)>n^\epsilon$ then implies $h(n)=P(n)$. Not covered: the endpoint $\epsilon=1/2$ and every smaller positive $\epsilon$, the existence of the densities $\delta_p$ of the first question, and the limit inferior of the second.

Acceptance. None on record. The site's label is OPEN (page last edited 24 September 2025), the curator had not commented on the claim as of 5 September 2026, and no publication, manuscript or named review was found in the search whose scope the problem page records. The listing describes the result as Lean-formalized but links no Lean source, build record or certificate, so no formalization link exists to record and none is listed as evidence. The library's reconstruction is this project's own reading, which does not accept an outside claim. A partial claim derives nothing for the problem's standing.

Depends on. No page of this wiki.