---

Claim. Xiyu Hu's manuscript "A Super-Square-Root Lower Bound for Factorial Residues Modulo a Prime" (in the author's GitHub repository, published 2026-07-23; the link pins the revision of the same day) proves that, for $A_p=\{k!\bmod p:1\le k<p\}$ as in Problem 478,

$$|A_p|\gg p^{8/15}.$$

The elementary bound is $|A_p|\gg p^{1/2}$, since every nonzero residue is a quotient of two factorials, and the best published constant is $(\sqrt2-o(1))p^{1/2}$ ([GSSV24], carded at Grebennikov, Sagdeev, Semchankau and Vasilevskii 2024). The argument uses three consecutive factorials: in $\mathbb F_p$ one has $(n+2)!=(n+1)!+((n+1)!)^2/n!$, so with $T_a(x)=a+a^2/x$ the factorial sequence supplies at least $p-2$ transitions $T_a(x)=y$ with $a$, $x$ and $y$ in $A_p$. After Cauchy–Schwarz the compositions $T_b\circ T_a^{-1}$ are affine maps; a multiplicity-two count bounds the repeated lines, and the point-line incidence bound of Stevens and de Zeeuw for Cartesian products (Bull. Lond. Math. Soc. 49 (2017); arXiv:1609.06284) gives the exponent $8/15$.

Submission note. Posted to erdosproblems.com as a proof claim by Xiyu Hu (account hxypqr) on 23 July 2026, giving "GPT-5.6 Sol" as the AI used:

For a prime $p$, let

$$A_p=\{k!\pmod p:1\leq k<p\}.$$

I prove the lower

bound

$$|A_p|\gg p^{8/15}.$$

Thus the exponent goes strictly beyond the

elementary square-root bound. This does not resolve the original Erdős problem: in particular, it does not prove positive density or the conjectured asymptotic

$$|A_p|\sim(1-1/e)p.$$

The main idea is to use three consecutive

factorials and the identity

$$(n+2)!=(n+1)!+\frac{((n+1)!)^2}{n!}$$

in

$\mathbb F_p$. Defining

$$T_a(x)=a+\frac{a^2}{x},$$

the factorial sequence

supplies at least $p-2$ transitions inside $A_p$. After applying Cauchy--Schwarz, the compositions $T_b\circ T_a^{-1}$ become affine lines. Then a multiplicity-two calculation, together with a incidence geometry result, the Cartesian-product point-line incidence theorem of Stevens and de Zeeuw, then gives the exponent $8/15$.

Covers. The lower bound $|A_p|\gg p^{8/15}$. It does not prove that $|A_p|\gg p$, nor the asymptotic $|A_p|\sim(1-1/e)p$ the problem asks for; the manuscript, its repository and the claim's summary all say so.

Depends on. No page of this wiki.

Formalization. The repository's lean/ folder is a Lean 4 development (Lean 4.29.0 with the matching Mathlib) whose theorem factorialResidues_cleared_eight_fifteenths proves $(p-2)^8\le(K+D^4)\,|A_p|^{15}$ from an explicit hypothesis named StevensDeZeeuwWeightedCorollary, the published incidence theorem left unformalized; the repository calls this a partial formalization, reports no sorry and no project axiom, and documents under docs/ which steps are checked and how the incidence theorem's hypotheses are met in the application. This corpus has not built the development, so the link is a formalization link and gives no formalized evidence.

Authorship and tools. Xiyu Hu is the manuscript's sole author and posted the claim. The repository's disclosure says that OpenAI's ChatGPT and Codex assisted with proof exploration, algebraic and literature checks, exposition, LaTeX preparation and the Lean development and are not authors; the forum entry names the system as GPT-5.6 Sol.

Standing. Posted on the problem's proof-claims tab as a partial claim on 2026-07-23 with the manuscript and the repository as its external links; the entry carried no comments. The repository says an arXiv submission is planned; none is recorded here. The manuscript is not refereed and no outside reviewer has recorded accepting it, so the claim is claimed. The site labels the problem OPEN (page last edited 12 April 2026) and its remarks do not mention the manuscript.