---

Claim. The module src/latest/ErdosProblems/Erdos4.lean of Boris Alexeev's lean-proofs repository (added 2026-08-26, pinned at the commit of 2026-09-15) proves Erdos4.erdos4 and Erdos4.erdos_4: for every real $C>0$ the set of $n$ with $p_{n+1}-p_n>C\log n\log_2n\log_4n/(\log_3n)^2$ is infinite, in the formal-conjectures form with zero-indexed primes. This is the question of Problem 4 answered yes. The same module proves Erdos4.fgkmt18: there are $C>0$ and $X_0$ such that for every real $X\ge X_0$ some consecutive-prime gap with right endpoint at most $X$ is at least $C\log X\log_2X\log_4X/\log_3X$, the bound of the 2018 five-author paper. The module Erdos4b.lean (added the same day) proves erdos_4, fgkmt18 and the index form fgkmt18_index by a second route. Neither file nor its note in the repository names an informal author, the repository's source list has no entry for them, and Erdos4.lean states that it asserts no historical novelty, so the development is recorded as the repository's own result. The repository's Erdos4Tilted module, which declares itself a formalization of DottedCalculator's manuscript, is a formalization link on that claim page.

Depends on. Nothing in this wiki.

Standing. Claimed. No outside reviewer has examined the development, and this corpus has not built or audited it, so no formalized evidence is listed.