What was already known
Erdős and Graham had a polynomial lower bound. Konyagin’s stronger exponential-scale result concerned a related binomial-coefficient problem.
AI involvement
Wouter van Doorn and Quanyu Tang credit ChatGPT 5.5 Pro with the core idea of adapting Konyagin’s method. They wrote the final proof; Aristotle later formalized part of it.
ChatGPT conceived the core transfer of Konyagin's argument, while the authors wrote the final proof and Aristotle formalized it afterward.
Importance
Confirms Erdős’s superpolynomial-growth conjecture for this least n.
Limitations
The linked Lean theorem assumes the Baker–Harman–Pintz short-interval prime estimate as an axiom. It checks the new deduction relative to that input, not a fully formalized unconditional proof.
Technical verification
The authors report Lean formalization of their theorems, but the exact main_theorem in the linked Lean file assumes Baker–Harman–Pintz's short-interval prime estimate as axiom bhp. Thus the new deduction is machine checked relative to that external theorem; the unconditional statement is not fully formalized in this artifact.
Independent checking
The authors report Lean formalization of their theorems, but the exact main_theorem in the linked Lean file assumes Baker–Harman–Pintz's short-interval prime estimate as axiom bhp. Thus the new deduction is machine checked relative to that external theorem; the unconditional statement is not fully formalized in this artifact.
- Checker
- Lean 4 kernel in Aristotle's source-reported formalization
- Scope
- Theorem 1.1 lower bound with θ = 21/40, conditional on the Baker–Harman–Pintz prime-counting axiom
- Basis
- Reported by the linked checker
Human understanding
Van Doorn and Tang say the paper was entirely human-written and explain the transfer from Konyagin's method through the small, medium and large n cases.
Correction and publication history
Confirms Erdős’s superpolynomial-growth conjecture for this least n.
Read this published revision