> ## Content Index > Fetch the complete content index at: https://www.digitalbrain.news/llms.txt > Use this file to discover other available public pages before exploring further. # Axiom formaliza en Lean 4 el teorema de los huecos entre primos con revisión humana - URL: https://www.digitalbrain.news/noticias/axiom-lean-4-teorema-246-huecos-primos/ - Published: 2026-08-19T14:30:22.000Z - Updated: 2026-08-20T07:41:48.000Z - Description: Axiom Math ha publicado la formalización completa en Lean 4 del teorema que dice que existen infinitos pares de primos consecutivos separados por 246 o… - Author: Ramón Pérez Coronado - Tags: #noticias, matematicas-ia, investigacion Axiom Math ha publicado [la formalización completa en Lean 4](https://primegaps.axiommath.ai/?ref=digitalbrain.news) del teorema que dice que existen infinitos pares de primos consecutivos separados por 246 o menos. Es uno de los resultados más celebrados de la teoría de números de la última década, y hasta ahora vivía en artículos revisados por humanos, no en código que una máquina pueda verificar línea a línea. ## Puntos clave - El resultado formalizado: hay infinitos n tales que p(n+1) menos p(n) es menor o igual que 246. - Construido sobre Mathlib y sobre trabajo previo de Kontorovich y Tao. - Más de 43 participantes entre matemáticos, ingenieros e investigadores principales. - El código se ha empaquetado en una librería reutilizable, PrimeGapsLib. - La demostración la genera AxiomProver, pero el plano y la revisión son humanos. ## Qué es el 246 y de dónde viene La conjetura de los primos gemelos dice que hay infinitos pares de primos separados por 2 (11 y 13, 17 y 19). Sigue sin demostrarse. Lo que sí se ha demostrado es una versión más débil y muy trabajosa: que hay algún hueco finito que se repite infinitas veces. Yitang Zhang lo consiguió por primera vez en 2013\. James Maynard lo bajó a 600 con una criba multidimensional. El proyecto colaborativo Polymath8b lo dejó en 246, que es donde sigue. Formalizar eso significa reescribir toda esa maquinaria en un lenguaje que un ordenador comprueba sin fiarse de nadie. Si compila, el teorema es correcto. No hay paso "y de aquí se sigue fácilmente" que nadie haya verificado. ## Cómo lo han hecho El proceso descrito tiene tres capas y ninguna sobra. Primero, el plano. Personas escriben el mapa de dependencias: qué lemas hacen falta, en qué orden, qué se apoya en qué. Es el trabajo de arquitectura y sigue siendo humano. Segundo, AxiomProver genera las demostraciones de cada pieza. Tercero, revisión humana y curación del código resultante hasta convertirlo en PrimeGapsLib, una librería que otros pueden reutilizar. Han formalizado por el camino el artículo de Maynard de 2015 sobre cribas multidimensionales y el de Polymath8b de 2014 sobre variantes de la criba de Selberg. Eso no es un teorema suelto: es infraestructura. ## Lo que se puede afirmar y lo que no Conviene decirlo claro porque este tipo de anuncio se cuenta mal con facilidad. La IA no ha demostrado nada nuevo. El teorema es de 2014 y lo demostraron matemáticos humanos. Lo que ha hecho aquí el sistema es traducir una demostración conocida a código verificable, que es un trabajo enorme, tedioso y donde tradicionalmente se tarda años. Formalizar resultados de este calibre ha sido históricamente el cuello de botella de todo el campo de la demostración asistida. Y hay 43 personas firmando el proyecto. Eso también dice algo sobre cuánto trabajo humano sigue haciendo falta. ## Por qué importa fuera de las matemáticas Porque Lean verifica, no opina. Un modelo que escribe una demostración en Lean o compila o no compila, y ese sí o no lo da el compilador, no otro modelo. Ese es el patrón que interesa a cualquiera que quiera usar IA en algo donde equivocarse cuesta dinero: poner al modelo a trabajar contra un verificador duro. En matemáticas es Lean. En desarrollo es la suite de tests y el tipado. En finanzas es la conciliación que tiene que cuadrar al céntimo. Cuando existe ese verificador, puedes dejar que el modelo genere mucho y descartar lo que no pasa. Cuando no existe, alguien tiene que leerse todo lo que genera, y ahí es donde los proyectos se atascan. La pregunta útil antes de automatizar un proceso con IA no es qué modelo usar. Es qué compilador tiene ese proceso. Si no tiene ninguno, el primer trabajo es construirlo. --- **Relacionado** [![Un residente de neurocirugía resuelve con GPT-5.6 una conjetura matemática abierta desde 2004](https://storage.ghost.io/c/6d/e3/6de31f63-d0a8-45df-9c6a-481016520347/content/images/size/w300/format/webp/2026/08/crouzeix-conjetura-resuelta-gpt-5-6-residente-neurocirugia.png)Un residente de neurocirugía resuelve con GPT-5.6 una conjetura matemática abierta desde 2004](https://www.digitalbrain.news/noticias/crouzeix-conjetura-resuelta-gpt-5-6-residente-neurocirugia/)[![Un aviso en el prompt de sistema basta para frenar las ideas que se contagian entre agentes](https://storage.ghost.io/c/6d/e3/6de31f63-d0a8-45df-9c6a-481016520347/content/images/size/w300/format/webp/2026/08/mind-viruses-ideas-autopropagadas-agentes-ia.png)Un aviso en el prompt de sistema basta para frenar las ideas que se contagian entre agentes](https://www.digitalbrain.news/noticias/mind-viruses-ideas-autopropagadas-agentes-ia/)