💻 computer science

The set of primes is supernatural: a Lean formalization of the statement of the conjecture

Este artículo presenta una formalización completa y verificada por máquina en Lean 4 de la conjetura de que ninguna función no constante construida a partir de la identidad, constantes y un número finito de operaciones puntuales (suma, multiplicación, exponenciación) mapea cada entero positivo a un número primo, transformando así la conjetura en un objetivo preciso y verificable por el núcleo para los sistemas de razonamiento automatizado.

Autores originales: A. Mayeux

Publicado 2026-08-11

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: A. Mayeux

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina una vasta e infinita biblioteca donde cada libro es un número. En esta biblioteca, hay un club muy especial y exclusivo llamado "los Primos". Estos son números que no pueden ser construidos multiplicando números más pequeños; son los átomos indivisibles de la aritmética, como el 2, 3, 5 o 7. Durante siglos, los matemáticos han intentado escribir una receta única y sencilla —una máquina hecha de herramientas matemáticas básicas— que pudiera escupir solo a estos miembros especiales del club. Querían una máquina que, sin importar qué número le alimentaras, siempre entregara un número Primo.

Las herramientas permitidas en esta receta son las más básicas que conocemos: sumar números, multiplicarlos y elevarlos a potencias (como elevar al cuadrado o al cubo). Puedes combinar y mezclar estas herramientas tanto como quieras, pero no puedes usar nada sofisticado como la división o las raíces cuadradas. La gran pregunta es: ¿Existe una forma de construir una máquina usando solo estas herramientas simples que nunca cometa un error? ¿Podría tal máquina generar una lista interminable de primos, o eventualmente tropezará y producirá un número que no sea primo? Esto no es solo un juego; toca el corazón mismo de cómo se estructuran los números. Si tal máquina existiera, significaría que los primos siguen un patrón simple y predecible. Si no, significa que los primos son salvajes, caóticos y "sobrenaturales" de una manera que desafía las fórmulas simples.

Este artículo es una historia de detectives digital sobre esa misma pregunta. El autor, Arnaud Mayeux, ha tomado un artículo matemático específico que proponía una conjetura audaz y lo ha traducido íntegramente a un lenguaje de programación llamado Lean. Piensa en Lean como un árbitro superestricto que revisa cada uno de los pasos de una demostración matemática para asegurar que es 100% lógicamente sólida, sin dejar lugar al error humano o a los momentos de "creo que esto funciona". El artículo no resuelve el misterio de si la máquina generadora de primos existe; en su lugar, construye un modelo digital perfecto e inquebrantable de las reglas del juego.

El hallazgo principal de este trabajo es que toda la teoría detrás de la conjetura de la "Máquina de Primos" ha sido codificada exitosamente en la computadora. Cada definición, cada ejemplo y cada tabla de números del artículo original vive ahora dentro de este archivo digital. El autor verificó 89 ejemplos diferentes de estas "funciones naturales" (el nombre elegante para las máquinas construidas a partir de suma, multiplicación y potencias). Para cada una, la computadora calculó los resultados y confirmó que todas fallan eventualmente en producir un número primo. Por ejemplo, una función funcionó perfectamente para los primeros seis números, pero se rompió en el séptimo. La computadora probó estos fallos con absoluta certeza, utilizando certificados digitales avanzados para verificar números enormes que a un humano le tomaría años revisar a mano.

Sin embargo, el artículo es muy claro sobre lo que no ha hecho. No ha demostrado que la Máquina de Primos sea imposible. No ha encontrado la respuesta definitiva. La conjetura central —que no existe tal máquina— sigue siendo un problema abierto, un "problema abierto con nombre" en el código de la computadora, esperando a que un humano o una inteligencia artificial finalmente lo demuestre. El artículo esencialmente dice: "Aquí está el libro de reglas exacto, y aquí está la evidencia de que cada máquina que hemos probado hasta ahora falla, pero el veredicto final aún no se ha emitido".

El autor también expandió el juego ligeramente. Preguntó: "¿Qué pasa si añadimos algunas herramientas más, como los factoriales (multiplicar un número por todos los números por debajo de él) o las flechas de Knuth (una forma de escribir potencias gigantescas)?". Construyó una nueva y más grande clase de máquinas con estas herramientas extra y planteó una nueva conjetura, aún más difícil: que incluso con estas súper-herramientas, todavía no se puede construir una máquina que solo fabrique primos. Esta nueva conjetura también queda abierta, sin demostrar, pero ahora está escrita de una manera que una computadora puede verificar si alguien logra encontrar la demostración.

En resumen, este artículo es un acto masivo de traducción y verificación. Toma una idea matemática compleja sobre la naturaleza caótica de los números primos y la encierra en una bóveda digital donde cada regla es verificada por una máquina. Confirma que, para cada ejemplo específico probado, la "Máquina de Primos" falla, pero deja la pregunta definitiva de si tal máquina es teóricamente posible como un desafío para el futuro. Los primos, al parecer, son de hecho "sobrenaturales", resistiéndose a cualquier fórmula simple con la que intentemos atraparlos.

Resumen Técnico: El conjunto de los primos es sobrenatural: Una formalización en Lean de la declaración de la conjetura

Planteamiento del problema
El artículo aborda la formalización de la "Conjetura de los Primos Sobrenaturales" propuesta originalmente en [3]. La conjetura postula que ninguna función no constante, construida a partir de la función identidad y constantes mediante un número finito de adiciones, multiplicaciones y exponenciaciones puntuales, mapea cada entero positivo a un número primo. El objetivo del artículo es traducir esta conjetura y su marco teórico circundante a una formalización verificada por máquina utilizando Lean 4 y la biblioteca Mathlib. El objetivo es establecer un objetivo preciso y verificado por el núcleo (kernel) para la conjetura, permitiendo que tanto sistemas de razonamiento humano como automatizado intenten una demostración.

Metodología
La formalización se contiene enteramente dentro de un único archivo de Lean 4, SPCL.lean (aproximadamente 1200 líneas), que depende únicamente de Mathlib. La metodología consiste en una traducción directa y exhaustiva del artículo fuente [3] a Lean, asegurando que cada definición, ejemplo, observación, resultado numerado y fila de tabla experimental tenga una contraparte verificada por máquina.

Componentes técnicos clave incluyen:

Estructuras de Elevación: El artículo axiomatiza las compatibilidades de la adición, multiplicación y exponenciación como una "estructura de elevación" (una 4-tupla $(E, +, \times, \wedge)$ ). Esto se formaliza como una clase de tipos (type class), y la categoría de tales estructuras se construye con leyes de identidad y composición.
Funciones Naturales: Se implementan dos codificaciones equivalentes de "funciones naturales":
1. Construcción de Palabras: Las funciones son generadas por palabras finitas sobre el alfabeto $\{A_+, A_\times, A_\wedge\}$ aplicadas al conjunto de funciones identidad y constantes.
2. Cierre Inductivo: Se define un predicado inductivo IsNatural con constructores para la identidad, constantes y las tres operaciones.
  La equivalencia entre estas dos definiciones se demuestra formalmente.
Formulación de la Conjetura: La conjetura se establece como una proposición con nombre (Conjecture_2_1) de tipo Prop sin una demostración. Se define explícitamente como una hipótesis en lugar de un teorema con sorry (pendiente), asegurando que la formalización no introduce nuevas suposiciones.
Verificación Experimental: El artículo formaliza 89 resultados experimentales de [3, §4]. Estos se establecen como teoremas que afirman la primalidad de valores específicos de funciones hasta cierto punto y la composición del primer valor no primo.
- Para valores más pequeños, las demostraciones dependen de norm_num (evaluación computacional).
- Para valores grandes (por ejemplo, $2^{2^6} + 93$ ), la formalización utiliza certificados de primalidad de Lucas. Estos se verifican mediante un lema personalizado lucasCert que comprueba las condiciones $a^{p-1} \equiv 1 \pmod p$ y $a^{(p-1)/q} \not\equiv 1 \pmod p$ para factores primos $q$ de $p-1$ , utilizando el táctico reduce_mod_char de Mathlib.

Contribuciones Clave

Formalización Exhaustiva: El artículo proporciona una formalización completa y "libre de sorries" de todo el artículo [3]. Cada definición, lema, proposición y fila de tabla está presente en el código de Lean.
Objetivo de Conjetura Preciso: Al establecer la conjetura como un Prop nombrado y no probado, el trabajo crea un objetivo específico y verificable para los sistemas de razonamiento automatizado. La estructura de dependencia es transparente; cualquier prueba de la conjetura dependería únicamente de las definiciones formalizadas y los axiomas de Lean/Mathlib.
Extensión Matemática: La formalización extiende la teoría de [3, Observación 3.4] definiendo una clase más amplia de funciones, IsNaturalKnuthFactorialSub. Esta clase incluye:
- La notación de flecha de Knuth (donde el nivel de la flecha es en sí misma una función en la clase).
- La función factorial.
- Resta truncada (bajo la condición $g(n) < f(n)$ ).
  El artículo demuestra que la clase original de funciones naturales se incrusta en esta clase extendida.
Verificación de Casos Probados: La formalización incluye pruebas para los casos donde la conjetura se cumple (por ejemplo, polinomios no constantes, formas lineales-exponenciales y la función de Fermat), utilizando resultados de teoría de números estándar de Mathlib (por ejemplo, divisibilidad polinómica, Teorema de Fermat Menor).

Resultados

Consistencia Formal: El archivo SPCL.lean compila en aproximadamente 30 segundos. Depende solo de los axiomas clásicos estándar de Lean (extensionalidad proposicional, corrección de cocientes, elección) heredados de Mathlib.
Tablas Experimentales: Las 89 filas de las tablas experimentales de [3] están formalizadas como teoremas. Las demostraciones para las afirmaciones de primalidad de valores grandes se verifican mediante certificados de Lucas comprobados por el núcleo, eliminando el riesgo de errores de transcripción en las cadenas de factorización.
Equivalencias Teóricas: La formalización demuestra la equivalencia entre la formulación funcional de la conjetura y su reformulación teórica de conjuntos (que el conjunto de los primos es "sobrenatural", lo que significa que no contiene ningún subconjunto natural infinito).
Consecuencias: Condicional a la conjetura, la formalización demuestra que el conjunto de los números de Fermat compuestos es infinito y que el conjunto de los valores no primos para cualquier función natural no constante es infinito.

Significado
El artículo afirma que su principal significancia radica en la rigurosidad y completitud de la formalización. Transforma un "desafío difícil para cualquier tipo de inteligencia" (como se describe en [3]) en un objetivo preciso y verificable por máquina. Al eliminar toda ambigüedad y asegurar que cada paso sea verificado por el núcleo de Lean, el trabajo permite que los sistemas de razonamiento automatizado intenten una demostración de la conjetura sin el riesgo de error humano en las definiciones subyacentes. El artículo no pretende resolver la conjetura, sino proporcionar la infraestructura necesaria para que una solución sea validada. También demuestra la viabilidad de formalizar conjeturas complejas de teoría de números impulsadas experimentalmente dentro del ecosistema de Mathlib.

Más como este