OpenAI formaliza en Lean 4 que los primos gemelos distan a lo sumo 186
GPT-6-Astra: infinitely pairs of consecutive primes with distance at most 186
OpenAI ha publicado una formalización en Lean 4 de un resultado sobre la distribución de los números primos: hay infinitos pares de primos consecutivos con una distancia de a lo sumo 186. La prueba se apoya en tres axiomas explícitos, incluidas estimaciones de tipo Deligne y un certificado numérico en Python. El desarrollo demuestra la conjetura DHL(40,2) y la aplica a un conjunto admisible de 40 enteros, obteniendo la cota para los gaps primos. Aunque los resultados son condicionales, el proyecto incluye verificación con Lean y un comparador que valida las pruebas.
El desarrollo deriva DHL(40,2) a partir de los siguientes supuestos: todo conjunto admisible de cuarenta desplazamientos enteros tiene infinitas traslaciones que contienen al menos dos primos.