El repositorio openai/PrimeGaps186, alojado en GitHub, contiene una formalización en Lean 4 que establece, de manera condicional, que el límite inferior del mayor hueco entre primos consecutivos es como máximo 186, junto con un certificado numérico en Python que respalda los cálculos intermedios. Los resultados en Lean dependen de tres axiomas explícitos —dos relativos a sumas de Kloosterman y uno sobre cotas de integrales físicas— que, según el repositorio, están demostrados en la literatura matemática citada (trabajos de Deligne, Katz, Fouvry, Kowalski y Michel), pero que no se han convertido en pruebas dentro del propio desarrollo de Lean. Las declaraciones principales, reunidas en el espacio de nombres PrimeGap186 dentro de PrimeGaps186.lean, son dhl_40_2, infinite_two_prime_translates_admissibleTuple y primeGapLiminf_le_186, esta última el enunciado que acota los huecos consecutivos entre primos. El certificado en Python, ejecutable con prime_gap_186_certificate.py, recomputa el ensayo completo desde cero —fue probado con Python 3.12.13, NumPy 2.2.6, python-flint 0.9.0 y una compilación personalizada de FLINT 3.6.0 con convolución corregida para polinomios con signo— y debe superar comprobaciones obligatorias de coma flotante y de convolución con signo para producir un justificante con passed: true; una ejecución exitosa no descarga ningún axioma de Lean. El proyecto fija Lean 4.34.0-rc2 y sus dependencias de Mathlib, y se compila sin errores ni advertencias; los comparadores Challenge.lean, Nanoda y el kernel de Lean aceptaron las pruebas en una máquina virtual Colima con Linux. La configuración del comparador admite los seis axiomas documentados del proyecto (los tres propios más propext, Quot.sound y Classical.choice), por lo que verifica pruebas condicionales, no los axiomas mismos. El repositorio se distribuye bajo licencia Apache 2.0, con los avisos de terceros ya incluidos.
Noticias agregadas con IA