La IA de Axiom Math verifica el teorema de los huecos primos de 246 en Lean

Axiom Math dice que su sistema AxiomProver ha producido una prueba en Lean 4 verificada por máquina del resultado más fuerte conocido sobre los huecos entre números primos: el teorema de que infinitos pares de primos difieren en no más de 246. La empresa publicó el resultado el 17 de agosto de 2026 como un plano de formalización interactiva acreditado a 41 colaboradores nombrados en matemáticas, ingeniería e investigación principal, con IEEE Spectrum reportando primero el hito.

El límite de 246 es el borde actual del conocimiento humano en el largo ataque a la conjetura de los primos gemelos, la hipótesis del siglo XIX de que los primos separados exactamente por dos aparecen para siempre. La página del proyecto de Axiom Math describe el trabajo como una formalización unificada del artículo de James Maynard de 2013 “Small gaps between primes” junto con la parte del seguimiento de la colaboración Polymath8b que redujo el límite de Maynard de 600 a 246. Las pruebas verificadas por máquina están organizadas en una biblioteca pública de Lean, PrimeGapsLib, con el teorema de 246 como su resultado insignia.

“Este teorema representa actualmente el umbral del conocimiento humano sobre los números primos”, dijo Ken Ono, matemático fundador de Axiom Math.

La verificación formal significa traducir una prueba a un lenguaje que un pequeño programa de confianza llamado kernel puede revisar línea por línea. El resultado no es una garantía absoluta — la declaración misma debe traducirse correctamente y el verificador debe ser sólido — pero elimina la falibilidad del árbitro humano de la cadena. Hasta ahora, los sistemas de IA que compiten en benchmarks de matemáticas se han medido mayormente en problemas de competición con pruebas cortas y autocontenidas; la brecha entre esos resultados y la formalización a nivel de investigación ha sido amplia, un patrón visible en sistemas anteriores que sobresalieron en geometría olímpica mientras dejaban la matemática de investigación en gran medida intacta.

De 70 millones a 246

La conjetura misma, formulada precisamente por Alphonse de Polignac en el siglo XIX, sigue sin probarse. El primer límite finito de cualquier tipo llegó en 2013, cuando Yitang Zhang demostró que infinitos pares de primos caen dentro de 70 millones entre sí. Meses después, Maynard introdujo un método de cribado refinado y redujo el límite a 600 — trabajo que contribuyó a su Medalla Fields 2022 — y la colaboración Polymath8b, que incluyó a Maynard y a Terence Tao, lo llevó a 246. El plano de Axiom Math expone esa progresión como el proyecto que se propuso formalizar.

La formalización sigue una cadena de procesos que la empresa describe en tres etapas. Los investigadores primero escribieron la prueba como un plano — cada definición, lema y teorema con una etiqueta, una declaración precisa y una lista de los resultados de los que depende — produciendo un grafo de dependencias que ordenó el trabajo. AxiomProver, el sistema multi‑agente de la compañía para la investigación matemática mediante pruebas formales, generó entonces pruebas en Lean 4 verificables por máquina basadas en Mathlib, la biblioteca comunitaria de matemáticas, y en PrimeNumberTheoremAnd, el proyecto de formalización existente liderado por Alex Kontorovich y Tao. El equipo de Axiom revisó el código generado y lo organizó en PrimeGapsLib.

Los resultados principales declarados por la biblioteca van un poco más allá del teorema principal. Además del límite de 246, formaliza el límite de 600 de Maynard, e incluye un desafío de verificación autocontenido — construido solo sobre Mathlib, con la ranura de la prueba dejada vacía — que permite a cualquiera con la herramienta comparadora de Lean confirmar de forma independiente que las pruebas de la biblioteca coinciden con los teoremas declarados. La empresa advierte que la verificación completa puede llevar horas; una versión reducida que cubre los otros dos resultados se ejecuta en minutos.

Dónde se sitúa esto entre las afirmaciones de formalización de IA

El resultado aparece en un año de crecientes afirmaciones sobre sistemas de IA que realizan matemáticas de nivel de investigación, la mayoría ancladas a puntajes de competición o pruebas cortas. Axiom Math ha sido uno de los reclamantes más agresivos: AxiomProver se acredita con la resolución de problemas previamente abiertos, incluido trabajo que la compañía ha publicado en revistas revisadas por pares, y los sistemas de IA ahora han resuelto varios problemas de Erdős de larga data. La formalización de 246 es un tipo diferente de resultado — no un nuevo teorema, sino una reconstrucción verificada por máquina de una de las pruebas más técnicamente exigentes de la teoría de números moderna.

La comparación más cercana es a principios de este año, cuando Math, Inc. utilizó su agente Gauss para completar la prueba formal de los resultados de empaquetamiento de esferas premiados con la Medalla Fields por Maryna Viazovska en las dimensiones 8 y 24. Sidharth Hariharan, estudiante de doctorado en Carnegie Mellon que lideró el esfuerzo humano del plano en esa formalización y que ahora es interno en Axiom Math y colaborador matemático nombrado en el proyecto de 246, sostiene que el nuevo resultado es el logro más integral. Su razonamiento, como él lo describió, es que Axiom se construyó para reutilización: en lugar de una formalización puntual de una sola prueba, PrimeGapsLib es una biblioteca mantenida de resultados sobre huecos primos destinada a apoyar trabajos y investigaciones de formalización futuros.

Esa distinción importa para la forma en que debe leerse el resultado. Una verificación puntual demuestra que un sistema puede sobrevivir al contacto con una prueba difícil. Una biblioteca muestra algo más cercano a una infraestructura — maquinaria formal reutilizable que otros resultados pueden aprovechar — que es la dirección en la que los sistemas de prueba formal han estado avanzando a medida que pasan de resolver ejercicios a comprobar matemáticas reales. La afirmación de capacidad aquí se basa en artefactos que son públicos y re‑ejecutables, más que en una puntuación de benchmark: el plano, el código Lean y un desafío comparador diseñados para que investigadores externos puedan verificar las pruebas por sí mismos.

Ono enmarca la matemática como un banco de pruebas para una ambición mayor. Si las propiedades del software — si un programa termina, si su salida es correcta para cada entrada — pueden expresarse como declaraciones matemáticas precisas, entonces los sistemas derivados de AxiomProver podrían probarlas formalmente, argumenta, señalando hacia la verificación del código generado por IA que comienza a operar en infraestructuras, finanzas y sistemas de seguridad.

“El mundo está a punto de funcionar con código informático que nadie ha leído”, dijo Ono. “La IA está aquí y ya no podemos mirar hacia otro lado — la formalización de pruebas es un banco de pruebas para resolver lo que creo que es el desafío más importante que enfrentaremos de la IA”.

Por ahora el entregable es más estrecho y verificable: un plano de 41 autores, una biblioteca pública de Lean y una prueba verificada por máquina de que los primos dentro de 246 entre sí nunca se agotan — el vecino verificado más cercano de la conjetura de los primos gemelos, y la pieza de investigación matemática más profunda que un sistema de IA ha comprobado de extremo a extremo.