{"id":"palomar/PALOMAR-2026-08-27-000003","url":"https://github.com/GrgAakash/factorial-hypergraph-auxiliary-erdos/tree/67b4088fc84422c84f7e5e205552757c3c0c9a71","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000003-v1.json","repo":"https://github.com/GrgAakash/factorial-hypergraph-auxiliary-erdos","tags":["math.NT","math.CO","msc:11N36","msc:11B65","msc:11A41","msc:05C65","number-theory","prime-numbers","lean","erdos-problems"],"score":0,"title":"GrgAakash/factorial-hypergraph-auxiliary-erdos","trust":"high","domain":"math.NT","source":"palomar","authors":["Aakash Gurung"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 formalization of a quantitative solution to the auxiliary problem suggested by Erdos alongside Problem 1059. Conditional on an explicitly stated standard dimension-one upper-bound sieve theorem, the formalization proves that for every sufficiently large L there are at least ((L+1)!)^eta/(100 log L) integers n in (2L!, (L+1)!] whose prime factors all exceed L and for which n-k! is composite for every 1 <= k <= L. The formalization does not prove that n is prime and therefore does not solve the original Erdos prime problem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"Factorial-residue hypergraphs and an auxiliary problem of Erdos","identifier":"","relationship":"formalizes"}]}