The board / number theory / #1058
Erdős Problem #1058
PROVEDdatabase updated 2025-09-28
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
`n` is a *solution* if `n ∈ [p_{k-1}, p_k)` for some `k` (with the convention `p_0 = 1`, where `p_1 = 2 < p_2 < ⋯` are the primes) and the only primes dividing `n! + 1` are `p_k` and `p_{k+1}`. Primes are indexed from `0` by `Nat.nth Nat.Prime`.
Let \(2=p_1<p_2<\cdots\) be the sequence of prime numbers. Are there only finitely many \(n\) such that \(n\in [p_{k-1},p_k)\) and the only primes dividing \(n!+1\) are \(p_{k}\) and \(p_{k+1}\)? A conjecture of Erdős and Stewart, as reported in problem A2 of Guy's collection [Gu04]. The only known cases are \(n=1,2,3,4,5\). Luca [Lu01] proved that indeed these are the only solutions.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/1058.Prizenone
Topicsnumber theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/1058
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.