This repository presents a Lean 4 formalization of a prime gap bound: liminf(p_{n+1}-p_n) ≤ 186. It derives this from the DHL theorem, using an admissible tuple of 40 integers. The core result is conditional, relying on three axioms: a Kloosterman sum bound, a correlation bound, and a numerical certificate.

The formalization includes a Python script that verifies the numerical inequalities. The Lean code is structured with declarations for the main theorem and supporting lemmas, and it has been checked in a Linux VM using Lean's kernel, accepting the stated axioms.