A formal proof of the Ramanujan--Nagell theorem in Lean 4

Este artículo presenta una formalización completa en Lean 4 del teorema de Ramanujan-Nagell, que establece que las únicas soluciones enteras a la ecuación $x^2 + 7 = 2^n$ son $(n,x) \in \{(3,\pm1),(4,\pm3),(5,\pm5),(7,\pm11),(15,\pm181)\}$, incluyendo la verificación de todas sus dependencias en teoría algebraica de números y describiendo la estrategia de prueba y los desafíos técnicos superados.

Lo esencial

Imagina que las matemáticas son como una inmensa biblioteca llena de libros antiguos. Algunos de estos libros contienen "recetas" o fórmulas que los genios del pasado, como el famoso matemático indio Srinivasa Ramanujan, escribieron en papel. Estas recetas son hermosas y parecen funcionar, pero a veces faltan los pasos intermedios o las explicaciones detalladas de por qué funcionan.

Este artículo es la historia de cómo un investigador, Barinder Banwait, decidió tomar una de esas recetas misteriosas y construirla ladrillo a ladrillo dentro de un ordenador, usando un lenguaje especial llamado Lean 4.

Aquí tienes la explicación sencilla de lo que hicieron:

1. El Misterio: La Receta de Ramanujan

En 1913, Ramanujan lanzó un desafío: "Si tomas un número, lo elevas al cuadrado, le sumas 7, y el resultado es una potencia de 2 (como 2, 4, 8, 16...), ¿qué números puedes usar?".
Ramanujan encontró 5 soluciones mágicas. Pero, ¿eran las únicas? ¿Había otras escondidas en el infinito?
En 1948, un matemático llamado Nagell demostró que sí, esas eran las únicas. Pero su demostración era como un mapa dibujado a mano: útil para un experto, pero lleno de saltos lógicos que un ordenador no podía entender automáticamente.

2. La Misión: Construir el Puente Digital

El objetivo de este trabajo fue traducir la demostración de Nagell a un lenguaje que el ordenador pudiera verificar paso a paso, sin dejar ni una sola duda. Es como si quisieras construir un puente entre dos islas (la teoría matemática y la realidad computacional) y asegurarte de que cada tabla esté atornillada perfectamente.

Para hacerlo, tuvieron que construir tres cosas fundamentales:

A. El Terreno (El Mundo de los Números Extraños)

La demostración requiere viajar a un "mundo" matemático especial llamado $\mathbb{Q}(\sqrt{-7})$.

• La Analogía: Imagina que los números normales (1, 2, 3...) viven en una ciudad plana. Pero para resolver este acertijo, tienes que entrar en una ciudad con un terreno muy peculiar, donde las reglas de la aritmética son un poco diferentes.
• El Reto: En los libros de texto, los matemáticos asumen que todos saben cómo caminar por este terreno. En el ordenador, tuvieron que dibujar el mapa completo: definir qué es el suelo, dónde están las casas (los números enteros) y cómo se mueven. Tuvieron que probar que en este terreno no hay "agujeros" y que cada número se puede descomponer en piezas únicas (como los átomos de los números).

B. La Llave Maestra (El Grupo de Unidades)

En este terreno especial, hay ciertos "números mágicos" (llamados unidades) que, si los usas, no cambian el tamaño de las cosas.

• La Analogía: Es como tener un juego de llaves. El libro de texto dice: "Solo hay dos llaves válidas: la positiva y la negativa". Pero para el ordenador, tuvieron que revisar cada cerradura posible y demostrar matemáticamente que no existen otras llaves que funcionen. Fue un trabajo tedioso, como revisar miles de candados uno por uno para asegurar que solo dos abren la puerta.

C. El Algoritmo de Verificación (La Prueba Final)

Una vez que tenían el mapa y las llaves, aplicaron la receta de Ramanujan.

• El Proceso: Usaron una herramienta llamada "expansión binomial" (una forma de descomponer números grandes) y la compararon con un reloj que marca cada 42 horas.
• El Resultado: El ordenador verificó que, si intentas usar cualquier otro número que no sea uno de los 5 originales, el reloj se desincroniza y la ecuación se rompe. ¡Solo los 5 números originales mantienen el reloj funcionando!

3. Los Obstáculos (Por qué fue tan difícil)

El autor explica que, aunque la matemática en papel parece elegante y fluida, convertirla en código fue como intentar traducir un poema a un idioma robótico:

• Diferentes "dialectos": A veces, el mismo número se escribe de dos formas distintas en el código (como decir "1+√-7 dividido por 2" vs "√-7 más 1 dividido por 2"). El ordenador no sabe que son lo mismo a menos que se lo expliques con un "puente" de traducción.
• La falta de "intuición": Un humano ve un paso y dice "obvio". El ordenador dice "¿por qué?". Tuvieron que escribir miles de líneas de código para explicar esos "obvios".
• La ayuda de la IA: Aquí entra un detalle moderno. El autor usó Inteligencia Artificial (como un asistente muy inteligente) para ayudarle a encontrar las herramientas correctas en la biblioteca de código y a escribir los pasos repetitivos. La IA no hizo la matemática por él, sino que actuó como un "arquitecto junior" que le pasó los ladrillos y le dijo: "Oye, para esta pared necesitas este tipo de cemento".

4. ¿Por qué importa esto?

Este trabajo es histórico por dos razones:

1. Es la primera vez que se formaliza completamente una conjetura de Ramanujan en un ordenador.
2. Demuestra que podemos usar ordenadores para verificar las matemáticas más profundas con una precisión absoluta, eliminando el riesgo de errores humanos.

En resumen:
Este artículo es el relato de cómo se tomó una idea matemática brillante pero abstracta, se desmenuzó en sus componentes más pequeños, se construyó un entorno digital seguro para ella y se usó un ordenador (ayudado por IA) para decir con total certeza: "Sí, Ramanujan tenía razón, y no hay ninguna otra solución oculta". Es la validación definitiva de una verdad matemática en la era digital.

Resumen técnico

Resumen Técnico: Una prueba formal del teorema de Ramanujan–Nagell en Lean 4

1. El Problema
El artículo aborda la formalización completa del Teorema de Ramanujan–Nagell, una ecuación diofántica exponencial planteada por Srinivasa Ramanujan en 1913. La ecuación es:
$$x^2 + 7 = 2^n$$
donde $x$ e $n$ son enteros. Ramanujan conjeturó que las únicas soluciones enteras ocurren para $n \in \{3, 4, 5, 7, 15\}$, lo que genera los pares $(n, x)$:
$$\{(3, \pm1), (4, \pm3), (5, \pm5), (7, \pm11), (15, \pm181)\}$$
Aunque Nagell demostró esto en 1948, el desafío de este trabajo es traducir la prueba matemática estándar (que utiliza teoría algebraica de números avanzada) a una prueba verificada por máquina dentro del asistente de pruebas Lean 4 y su biblioteca estándar Mathlib.

2. Metodología
La formalización se basa en la estructura de la prueba clásica (siguiendo a Stewart y Tall), pero requiere una infraestructura algebraica masiva para manejar los detalles que en las pruebas manuales se dan por sentados.

• Estructura del Código: La formalización se distribuye en cinco archivos Lean, organizados en dos capas:

  1. Infraestructura Algebraica (3 archivos): QuadraticIntegerROI.lean, RingOfIntegers.lean y FieldIsomorphism.lean. Estos definen el anillo de enteros del cuerpo cuadrático $K = \mathbb{Q}(\sqrt{-7})$, establecen su isomorfismo con representaciones alternativas y prueban propiedades fundamentales (discriminante, grupo de unidades, factorización única).
  2. Prueba Principal (2 archivos): Helpers.lean (propiedades algebraicas específicas) y Basic.lean (la lógica de la demostración: factorización, reducción módulo 42 y unicidad).

• Estrategia de Prueba Formalizada:

  1. Caso Par: Se resuelve directamente mediante factorización en $\mathbb{Z}$.
  2. Caso Impar: Se trabaja en el anillo de enteros $\mathcal{O}_K = \mathbb{Z}[\theta]$ donde $\theta = \frac{1+\sqrt{-7}}{2}$.
  3. Factorización Única: Se demuestra que $\mathcal{O}_K$ es un Dominio de Factorización Única (UFD) y un Dominio de Ideales Principales (PID), lo que permite descomponer la ecuación en factores irreducibles $\theta$ y $\theta'$.
  4. Reducción Modular: Mediante expansión binomial y reducción módulo 7, se demuestra que el exponente $m = n-2$ debe pertenecer a una de tres clases residuales módulo 42 ($m \equiv 3, 5, 13 \pmod{42}$).
  5. Unicidad: Se utiliza una argumentación de valoración $p$-ádica (específicamente 7-ádica) para demostrar que cada clase residual contribuye con a lo sumo una solución.

3. Contribuciones Clave
El autor presenta tres contribuciones principales:

• Prueba Verificada: La primera formalización completa de una conjetura de Ramanujan en un asistente de pruebas, resolviendo una ecuación diofántica exponencial específica sin axiomas no verificados (sorry).
• Infraestructura de Teoría Algebraica de Números: Desarrollo de una biblioteca reutilizable para anillos de enteros de cuerpos cuadráticos en Lean 4. Esto incluye:
  • Identificación rigurosa del anillo de enteros $\mathcal{O}_K$ para $d \equiv 1 \pmod 4$.
  • Cálculo del número de clases (demostrando que es 1, por lo tanto, es un PID).
  • Determinación del grupo de unidades ($\{\pm 1\}$).
  • Pruebas de irreducibilidad y coprimalidad de elementos específicos.
• Análisis de la Brecha Formal-Informal: Un estudio detallado de las diferencias entre las pruebas de libros de texto y las formalizadas, identificando dónde los argumentos informales requieren una elaboración sustancial (ej. transportar propiedades entre representaciones isomórficas de campos).

4. Resultados Técnicos y Estadísticas

• Código: El proyecto consta de 3,570 líneas de código y 125 declaraciones (definiciones, lemas, teoremas).
• Dependencias: Se basa en el commit 66ba1e1aecd9 de Mathlib (Lean 4.26.0-rc2).
• Verificación: La prueba depende únicamente de los tres axiomas estándar de Lean (propext, Classical.choice, Quot.sound).
• Gráfico de Dependencias: La prueba se estructura en un grafo de dependencias de ~70 nodos, donde la mayor parte del esfuerzo (aprox. 1,182 líneas en Helpers.lean) se dedica a establecer las invariantes algebraicas del anillo de enteros antes de abordar la ecuación diofántica en sí.

5. Desafíos y Lecciones Aprendidas
El artículo destaca varios obstáculos técnicos que no son evidentes en las pruebas manuales:

• Isomorfismos y Cerradura Integral: En Lean, diferentes presentaciones del mismo campo (ej. $\mathbb{Q}(\sqrt{-7})$ generado por $\sqrt{-7}$ vs. generado por $\frac{1+\sqrt{-7}}{2}$) son tipos distintos. Se requirió construir isomorfismos explícitos y transportar manualmente la propiedad de "cerradura integral" entre ellos.
• Inferencia de Clases de Tipos (Typeclass Diamonds): Conflictos entre instancias de álgebra (ej. QuadraticAlgebra vs. DivisionRing.toRatAlgebra) que requieren declaraciones manuales (letI, haveI) para que el compilador las reconcilie.
• Aritmética en $\mathcal{O}_K$: Operaciones triviales en $\mathbb{Z}$ (como simplificar $\theta^2 = \theta - 2$) requieren múltiples pasos de coerción y reescritura en Lean, ya que no existen procedimientos de decisión automáticos para anillos de enteros como los hay para enteros estándar.
• Rendimiento: Algunas pruebas (especialmente la determinación del grupo de unidades y la reducción módulo 42) requieren aumentar el límite de "latidos" (maxHeartbeats) a 400,000 o más debido a la complejidad computacional de los casos de fuerza bruta necesarios.

6. Significado e Impacto

• Primicia Histórica: Es la primera resolución completa de una ecuación diofántica exponencial específica en cualquier sistema de verificación formal.
• Rol de la IA: El proyecto destaca el uso significativo de herramientas de IA generativa (Claude Code y Aristotle) para sugerir tácticas, reparar pruebas tras actualizaciones de la biblioteca, descubrir lemas y generar código repetitivo. Esto sugiere que la IA asistida es crucial para reducir la barrera de entrada en la formalización de matemáticas avanzadas.
• Futuro de la Verificación: Demuestra que la infraestructura de Mathlib es lo suficientemente madura para manejar problemas complejos de teoría algebraica de números, estableciendo un precedente para formalizar conjeturas más profundas de Ramanujan y otros problemas en teoría de números.

En conclusión, este trabajo no solo valida un teorema clásico, sino que construye los cimientos necesarios para formalizar futuras investigaciones en teoría de números algebraicos dentro del ecosistema Lean.