Este repositorio presenta una formalización en Lean 4 de un límite de brecha prima: liminf(p_{n+1}-p_n)≤186. Se deriva del teorema DHL, utilizando una tupla admisible de 40 enteros. El resultado central es condicional, dependiendo de tres axiomas: una cota de suma de Kloosterman, una cota de correlación y un certificado numérico.

La formalización incluye un script de Python que verifica las desigualdades numéricas. El código Lean está estructurado con declaraciones para el teorema principal y lemas auxiliares, y ha sido verificado en una máquina virtual Linux usando el kernel de Lean, aceptando los axiomas mencionados.