本仓库提供了素数间隙界liminf(p_{n+1}-p_n)≤186的Lean 4形式化。它从DHL定理推导出该结果，使用了一个包含40个整数的可容许元组。核心结果是条件性的，依赖于三个公理：一个Kloosterman和界、一个相关性界和一个数值证书。该形式化包括一个Python脚本，用于验证数值不等式。Lean代码结构化了主定理和辅助引理的声明，并已在Linux虚拟机中使用Lean的内核进行了检查，接受了所述公理。