Claims

../

2022_04_03_grebennikov_sagdeev_semchankau_vasilevskii: Grebennikov, Sagdeev, Semchankau and Vasilevskii (Rev. Mat. Iberoam. 2024) prove that the factorials modulo p take at least (sqrt 2 + o(1)) sqrt p distinct values; refereed.

2026_07_23_hu: A manuscript proving that at least about p^(8/15) residue classes modulo a prime p are factorials, beyond the square-root bound, with a partial Lean formalization; it leaves positive density and the asked asymptotic open.

---