A formalization of the Gelfond-Schneider theorem

A continuación presento un resumen técnico detallado del artículo "A formalization of the Gelfond-Schneider theorem" en español, estructurado según los puntos solicitados.

1. El Problema: El Séptimo Problema de Hilbert

El artículo aborda la formalización en el asistente de pruebas Lean 4 (utilizando la biblioteca matemática Mathlib) del Séptimo Problema de Hilbert y su solución, conocida como el Teorema de Gelfond-Schneider.

• Contexto: La teoría de números trascendentes busca clasificar números reales en algebraicos (raíces de polinomios con coeficientes enteros) y trascendentes. Aunque se sabe que casi todos los números reales son trascendentes, demostrarlo para constantes específicas es extremadamente difícil.
• Enunciado del Problema: Hilbert preguntó en 1900 si números de la forma $\alpha^\beta$ son algebraicos o trascendentes, dado que $\alpha$ y $\beta$ son números algebraicos, excluyendo los casos triviales ($\alpha=0, 1$ o $\beta$ racional).
• El Teorema: Demostrado independientemente por Gelfond y Schneider en 1934, establece que si $\alpha$ y $\beta$ son números algebraicos, con $\alpha \neq 0, 1$ y $\beta$ irracional, entonces $\alpha^\beta$ es trascendente.
• Importancia: Este resultado es un pilar fundamental que conecta la teoría de números algebraicos con el análisis complejo, resolviendo casos como la trascendencia de $2^{\sqrt{2}}$, $e^\pi$ y $i^i$.

2. Metodología y Enfoque de Formalización

Los autores, Michail Karatarakis y Freek Wiedijk, han llevado a cabo una formalización completa y rigurosa que va más allá de la verificación de pasos aislados, construyendo la infraestructura necesaria desde cero.

A. Infraestructura Algebraica y Teoría de Números

• La "Casa" de un Número Algebraico (House): Definieron formalmente el concepto de house de un número algebraico ($|\alpha|$), que es el máximo módulo de sus conjugados. Para evitar problemas con tipos dependientes y la gestión de conjuntos no ordenados, utilizaron una inmersión canónica del cuerpo de números $K$ en un álgebra de Banach, tratando el house como una norma ($L^\infty$). Esto permitió usar las APIs de espacios normados de Mathlib para probar propiedades como la multiplicatividad y la desigualdad triangular de manera inmediata.
• Lema de Siegel para Cuerpos de Números: El núcleo de la prueba requiere la existencia de coeficientes "pequeños" (enteros algebraicos) para una función auxiliar. Formalizaron una versión generalizada del Lema de Siegel para el anillo de enteros $\mathcal{O}_K$ de un cuerpo de números. Esto se logró mediante un argumento de descenso: transformar el sistema lineal sobre $\mathcal{O}_K$ en un sistema más grande sobre los enteros $\mathbb{Z}$, resolverlo usando el Lema de Siegel clásico de Mathlib, y luego "levantar" la solución de vuelta a $\mathcal{O}_K$.

B. Construcción de la Función Auxiliar y Análisis Complejo

La prueba se basa en la construcción de una función auxiliar $R(z)$ que se anula en puntos específicos con alta multiplicidad.

• Sistema Lineal: Se define un sistema de ecuaciones lineales homogéneas para determinar los coeficientes de $R(z)$. Se utiliza el Lema de Siegel para garantizar la existencia de una solución no trivial con coeficientes acotados.
• La Función Global $S(z)$: Un desafío técnico mayor fue formalizar la función auxiliar global $S(z)$, que clásicamente se define como un cociente meromorfo con polos removibles en enteros. En Lean, las definiciones meromorfas parciales son problemáticas.
  • Solución: Los autores construyeron $S(z)$ como una función total y holomorfa por partes. Descomponen el dominio en los puntos singulares y su complemento. En los puntos singulares, utilizan expansiones de series de potencias locales para "reparar" la singularidad (definir el valor de la función donde el denominador se anula) y luego "pegan" (glue) estas definiciones locales con la fórmula racional global. Esto demuestra rigurosamente que $S(z)$ es analítica en todo el plano complejo.
• Acotación: Se establecen cotas superiores analíticas (usando la fórmula integral de Cauchy) y cotas inferiores aritméticas (usando la norma del cuerpo de números) para un valor derivado de la función.

C. Contradicción

La prueba finaliza mostrando una contradicción:

1. Cota Inferior (Aritmética): Si $\alpha^\beta$ fuera algebraico, el valor derivado $\rho$ sería un entero algebraico no nulo, lo que implica que su norma es $\ge 1$.
2. Cota Superior (Analítica): Mediante el análisis de la función $S(z)$, se demuestra que $|\rho|$ puede hacerse arbitrariamente pequeño al aumentar un parámetro $r$.
3. Resultado: Para $r$ suficientemente grande, la cota superior es menor que la cota inferior, lo que es imposible. Por tanto, la suposición de que $\alpha^\beta$ es algebraico es falsa.

3. Contribuciones Clave

• Primera Formalización: Este es el primer formalización del Teorema de Gelfond-Schneider en cualquier asistente de pruebas.
• Infraestructura en Mathlib: El proyecto ha integrado partes del código en la biblioteca principal de Mathlib, incluyendo definiciones de la "casa" de un número algebraico, versiones del Lema de Siegel para cuerpos de números y herramientas avanzadas de análisis complejo (funciones holomorfas por partes, manejo de singularidades removibles).
• Gestión Explícita de Constantes: A diferencia de las pruebas a mano que usan notación $O(\cdot)$, la formalización requirió construir explícitamente una secuencia de constantes ($c_1$ a $c_{15}$) dependientes del grado del cuerpo y las propiedades geométricas. Esto es crucial para la contradicción final y demuestra la viabilidad de métodos efectivos en este contexto.
• Verificación de Constantes Específicas: Como verificación de la corrección del marco, demostraron formalmente la trascendencia de la constante de Gelfond-Schneider: $\sqrt{2}^{\sqrt{2}}$.

4. Resultados

• Se ha verificado formalmente el teorema: theorem transcendental_cpow_of_isAlgebraic_of_irrational.
• Se ha demostrado la trascendencia de $\sqrt{2}^{\sqrt{2}}$ sobre $\mathbb{Q}$.
• Se ha establecido una base sólida para la teoría de números trascendentes en Lean, superando la etapa de resultados aislados (como la trascendencia de $e$ o $\pi$) hacia marcos teóricos más profundos.

5. Significado y Futuro

Este trabajo es un hito en la formalización de matemáticas avanzadas:

• Puente entre Áreas: Demuestra la capacidad de los asistentes de prueba para manejar la interacción compleja entre la teoría de números algebraicos y el análisis complejo.
• Extensibilidad: Los autores señalan que esta formalización sienta las bases para:
  • El Teorema de Baker sobre formas lineales en logaritmos (que generaliza Gelfond-Schneider).
  • La versión p-ádica del teorema (usando integrales de Schnirelmann en lugar de Cauchy).
  • Generalizaciones a curvas elípticas y funciones de Weierstrass $\wp$.
  • El Teorema de Schneider-Lang.
  • La verificación condicional de la Conjetura de Schanuel.
• Métodos Efectivos: La gestión explícita de constantes sugiere que en el futuro será posible desarrollar procedimientos de decisión automatizados para verificar la independencia lineal de logaritmos específicos, automatizando pruebas que actualmente son tediosas.

En resumen, este artículo no solo verifica un teorema histórico, sino que expande significativamente las fronteras de lo que es posible formalizar en teoría de números, proporcionando herramientas robustas para investigaciones futuras en trascendencia y análisis.