PrimeGaps186

该项目是对素数间隙上界≤186这一数学结论的条件化形式化验证，基于Lean 4定理证明语言实现。核心功能包括：形式化推导DHL[40,2]命题、构造直径为186的可容许素数组、并由此导出liminf(pₙ₊₁−pₙ) ≤ 186；技术特点是采用条件化建模——依赖三个明确列出的Kloosterman和估计公理（未在Lean中证明，但引自Deligne定理与Fouvry–Kowalski–Michel文献），辅以Python数值验证脚本提供计算支撑。适用于数论形式化验证、解析数论教学演示、以及对素数分布边界结果进行可信性复现与扩展研究。