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.
- ks2048
Contexto: según Wikipedia [0], hace apenas unos días alguien publicó una prueba de una cota de 240 [1].
- quuxplusone
¿Qué está tratando de decir esta jerigonza generada por IA? ¿Que hay infinitos pares de primos p,q con q=p+186?
La primera ecuación bajo "El resultado" parece decir que encontraron una secuencia infinita de primos cuya densidad es para siempre mayor que 1/186, lo cual no coincide con mi entendimiento de cómo funciona la densidad de primos.
- dang
Hilo relacionado en curso:
GPT-6 Astra - https://news.ycombinator.com/item?id=49554643
(ver también https://news.ycombinator.com/item?id=49555621 desde allí)