Prime gap

primeGapdef

The n-th prime gap is the distance from the n-th prime to the next one. The behaviour of this sequence — how small it gets infinitely often, how large it can be — is the subject of much of analytic number theory.

noncomputable def primeGap (n : ℕ) : ℕ :=
  Nat.nth Nat.Prime (n + 1) - Nat.nth Nat.Prime n

From Mathlib

Data.Nat.Nth
Data.Nat.Prime.Basic

import Conjectura.Defs.Mathematics.NumberTheory.PrimeGap · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits