OpenAI y la conjetura de primos gemelos: el modelo que estrecha la brecha

Un nuevo récord en la distancia entre primos consecutivos

OpenAI publicó este mes el repositorio PrimeGaps186 en GitHub, una formalización en Lean 4 acompañada de un certificado numérico en Python que demuestra, de forma condicional, que existen infinitos pares de primos consecutivos separados por 186 o menos. El nombre ya lo dice: mejora la cota hasta 186, el dígito central del esperado avance hacia primos gemelos — la conjetura que pide infinitos pares (p, p+2) lleva resistiéndose desde el siglo XIX.

Es la primera entrega pública de un proyecto que la compañía venía coqueteando en sombra: una pieza más del calendario de hitos de GPT-6 Astra, el modelo que OpenAI lanzó esta misma semana con la narrativa de la "era AGI" y que, según reportes de prensa, ya habría ayudado a avanzar en diez problemas abiertos de matemáticas y ciencias de la computación, todos verificados en Lean 4, según reportó Wccftech.

Qué dice exactamente el resultado

El corazón del repositorio es PrimeGaps186.lean, un archivo Lean 4 con tres declaraciones principales, todas dentro del namespace PrimeGap186:

🤖 La IA no es solo para leer sobre ella

En la comunidad la aplicamos: automatización, agentes IA y herramientas reales para emprender, no solo para informarte.

👥 Aplicarla en la comunidad

dhl_40_2: la variante DHL[40,2] —el tipo de objeto combinatorio que la estrategia Zhang–Maynard–Polymath8b convirtió en sinónimo de progreso contra la conjetura de primos gemelos.
infinite_two_prime_translates_admissibleTuple: la existencia de infinitos traslados de dos primos de un tuple entero admisible.
primeGapLiminf_le_186: la cota final, que afirma que el límite inferior de las diferencias p(n+1) − pn es, como mucho, 186.

La pieza clave combina dos elementos: una tupla explícita de diámetro 186 y un certificado numérico que verifica los ingredientes analíticos necesarios. Una tupla "admisible" es aquella que omite una clase de residuo módulo cada primo — la condición necesaria para que Zhang y Maynard pudieran tejer sus cribas hace una década.

El repositorio fija la versión a Lean 4.34.0-rc2 y describe el pipeline de verificación: lake exe cache get, luego lake build PrimeGaps186. Un comparator independiente (Challenge.lean más comparator/main.json) acepta las pruebas siempre que el entorno permita solo seis axiomas: los tres documentados por el proyecto, más propext, Quot.sound y Classical.choice.

El asterisco de los axiomas: lo que NO está probado

Aquí está la parte incómoda, y el propio README la deja clarísima: las pruebas de Lean son condicionales a tres axiomas explícitos que OpenAI no formaliza en el propio archivo.

Los tres axiomas son:

PrimeGap186.kloosterman3_bound, una cota de tipo Deligne para una suma de Kloosterman en tres variables. El repositorio lo atribuye a Nicholas M. Katz (Gauss Sums, Kloosterman Sums, and Monodromy Groups, Princeton, 1988, Teorema 4.1.1).
PrimeGap186.kloosterman2_correlation_bound, una cota para una suma de correlación que el README adjudica a Fouvry, Kowalski y Michel, The Friedlander–Iwaniec character sum, junio de 2013.
PrimeGap186.physical_integral_bounds, un conjunto de 104 cotas externas, 45 internas y tres "cap bounds" que respaldan la parte numérica del certificado.

Es decir: el repositorio demuestra la arquitectura lógica que conecta estos tres pilares con el resultado 186, pero los pilares en sí siguen siendo citas bibliográficas, no teoremas reinterpretados por la máquina. El comparator/main.json lo confirma con claridad: "this verifies conditional proofs, not the inputs themselves".

El certificado numérico en Python

Acompañando al Lean hay prime_gap_186_certificate.py, un script que recalcula desde cero la parte numérica de la verificación. Lo probaron con Python 3.12.13, NumPy 2.2.6, python-flint 0.9.0 y una build personalizada de FLINT 3.6.0 con una corrección en la convolución de polinomios con signo — un parche que no viene incluido en el repo.

El comando canónico, según el README, es:

python3 -B prime_gap_186_certificate.py --workers 4 --output prime_gap_186_fresh.json

El -B (deshabilitar el cache de bytecodes), el output fresco y la negativa a usar -O/-OO o PYTHONOPTIMIZE no son manías: son requisitos para que las "comprobaciones obligatorias de coma flotante y convolución con signo" pasen. Si todo cuadra, produces un recibo con passed: true. Pero el recibo solo certifica la parte numérica; los axiomas siguen siendo axiomas.

Por qué importa más allá de los primos

Hasta ahora, el récord de hueco entre primos consecutivos era 246, un número que lleva doce años sin moverse. Lo estableció la colaboración Polymath8b — en la que participaron el medallista Fields James Maynard y Terence Tao — sobre la base del trabajo original de Yitang Zhang (2013, hueco acotado por 70 millones) y del propio Maynard (2014, bajado a 600). Por eso 186, documentado en el repositorio de OpenAI, representa un salto porcentual relevante en una pared de más de una década.

Sin embargo, no es una verificación one-shot. Como recordó OfficeChai al cubrir el caso de la startup Axiom Math, que formalizó el récord 246 con su AxiomProver y publicó la librería PrimeGapsLib como infraestructura reusable, la tendencia del sector es construir bibliotecas compartidas — Mathlib, PrimeGapsLib y ahora potencialmente el código de OpenAI — donde cada nuevo resultado herede el andamiaje de los anteriores.

Otro ángulo clave: según IBTimes, la comunidad formalizadora en Lean ya supera los dos millones de líneas en Mathlib, con hitos públicos como la formalización del Liquid Tensor Experiment (Peter Scholze, 2022) y el Equational Theories Project coordinado por Tao en 2023-2024. Cada repositorio de este tipo es un paso más hacia una matemática en la que las afirmaciones importantes vienen con un "certificado de máquina" adjunto.

El trasfondo del lanzamiento: GPT-6 Astra

PrimeGaps186 no cae en el vacío. OpenAI lanzó GPT-6 Astra el mismo septiembre de 2026 — Wired lo describe como un modelo enfocado en uso del computador, navegación web y software engineering, con Greg Brockman asegurando que "ahora estamos en la era AGI" y Sam Altman hablando de un calendario de releases dominado por consideraciones de seguridad más que de capacidad.

Según Wccftech, en los benchmarks el Astra habría logrado 100% en ExploitBench, 98,6% en ARC-AGI-3 y 97,6% en FrontierMath Tier 4 v2; 9to5Mac añade que la versión anunció haber ayudado en diez problemas abiertos. Más allá de los puntajes — que requerirían contexto para comparar con fair play frente a harnesses especializados — la decisión de abrir el código (Apache 2.0) de PrimeGaps186 encaja con la narrativa de OpenAI de mover parte del progreso de IA hacia tareas verificables como las matemáticas formales.

¿Qué significa esto para tu startup?

Para un founder hispanohablante, los dividendos prácticos no están en la fórmula de primos, sino en tres tendencias que este lanzamiento acelera:

La verificación formal como feature de producto. Si tu software toca criptografía, fintech, salud o infraestructura crítica, internalizar Lean (o contratar a alguien que lo sepa) empieza a ser una inversión razonable, no un lujo académico. El costo marginal de "pasar tu código por un checker" cae cada año.
Modelos de IA como compañeros de investigación. Astra ayudando en diez problemas abiertos con verificación Lean es un caso temprano, pero el patrón se replica: del código a la matemática formal, el modelo se está convirtiendo en un colaborador más, no en un oráculo. Acción concreta: reserva una hora a la semana para experimentar con GPT-6 Astra (o el modelo equivalente que tengas disponible) sobre tu código más crítico — pidiéndole no solo que lo arregle, sino que lo pruebe formalmente.
"Trust by proof" como narrativa de marca. Si tu startup vende IA, software sensible o maneja datos confidenciales, apelar a verificación formal — aunque sea parcial, explicando qué axiomas quedan sin demostrar — te diferencia de los competidores que solo pueden hablar de "tests y QA manual".