An explicit prime gap under the Riemann hypothesis, formalized in Lean with its prime power input made elementary

Contributed by Steve Hubbard

Source files