A Lean formalization of a bound concerning long gaps between primes - View it on GitHub