🔢 mathematics

Formalizing $A_1^{(1)}$ Curve Neighborhoods in Lean 4

Este artículo presenta una formalización completa y sin axiomas en Lean 4 de los vecindarios de curvas combinatorios para el tipo $A_1^{(1)}$ , utilizando el sistema de Coxeter del grupo diedral infinito para verificar fórmulas explícitas y obtener una versión computable de estos vecindarios.

Autores originales: Yihe Huang, Sizhe Cui, Jiaqi Wang, Jujian Zhang

Publicado 2026-04-28

📖 3 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Yihe Huang, Sizhe Cui, Jiaqi Wang, Jujian Zhang

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

El Mapa de los Pasos Infinitos: Explicando la Formalización de "Vecindarios de Curvas"

Imagina que estás jugando a un videojuego de estrategia en un tablero que no tiene fin. En este juego, no te mueves por casillas cuadradas, sino que te mueves siguiendo reglas muy estrictas de "reflejos" y "giros". Este tablero es lo que los matemáticos llaman el Grupo Diédrico Infinito ( $D_\infty$ ).

1. El Problema: El laberinto de las reglas complicadas

En matemáticas, existe un concepto llamado "vecindarios de curvas". Imagina que estás en un punto del tablero y quieres saber: "Si solo puedo dar ciertos pasos (con un límite de energía o 'grado'), ¿hasta qué lugares puedo llegar y cuáles son los puntos más lejanos que puedo alcanzar?".

Calcular esto es como intentar resolver un laberinto gigante mientras alguien te dice: "Puedes moverte, pero cada paso debe seguir una lógica de simetría perfecta y no puedes gastar más de X cantidad de energía".

Los matemáticos ya tenían una fórmula para esto, pero las reglas son tan detalladas (hay que revisar si los pasos son pares o impares, si la longitud de la palabra es la correcta, etc.) que es extremadamente fácil cometer un error humano. Es como intentar hacer una cuenta de multiplicar de 20 dígitos mentalmente: un pequeño desliz y todo el resultado es basura.

2. La Solución: El "Árbitro de Hierro" (Lean 4)

Los autores de este artículo decidieron no confiar en la intuición humana. En lugar de eso, usaron una herramienta llamada Lean 4.

Imagina que Lean 4 no es una calculadora, sino un Árbitro de Hierro Infalible. Este árbitro no acepta un "creo que esto es así". El árbitro exige que cada paso, cada movimiento y cada regla esté escrito en un lenguaje lógico tan perfecto que sea imposible mentirle. Si hay un error en la lógica, el árbitro detiene el juego y dice: "Error. Esto no es verdad".

Lo que hicieron los investigadores fue "traducir" todo el mundo de estas matemáticas complejas al lenguaje de este Árbitro. No solo escribieron la respuesta, sino que construyeron el tablero, las reglas de movimiento y la lógica de la energía dentro de la mente del Árbitro.

3. ¿Qué lograron exactamente?

El trabajo tuvo tres grandes éxitos:

La Verificación Total: Demostraron que la fórmula que los matemáticos usaban antes es 100% correcta. El Árbitro de Hierro revisó cada detalle y dio el visto bueno. No hay margen de error.
El Puente entre la Teoría y la Acción: A veces, las matemáticas son tan abstractas que solo existen en el papel. Los autores lograron que estas reglas fueran "computables". Es decir, transformaron una idea filosófica sobre formas y curvas en un programa de computadora real que puedes ejecutar para obtener resultados exactos.
Un Mapa que Funciona: Al final, crearon una herramienta donde tú le das un punto de partida y una cantidad de "energía", y la computadora te dice exactamente cuáles son los límites de tu territorio sin equivocarse jamás.

En resumen...

Si las matemáticas tradicionales son como intentar dibujar un mapa de un mundo infinito a mano (donde siempre puedes fallar en una línea), este trabajo es como programar un GPS ultrapreciso que entiende las leyes de ese mundo infinito y te garantiza que nunca te perderás.

Resumen Técnico: Formalización de Vecindades de Curvas de tipo $A_1^{(1)}$ en Lean 4

Problema
El estudio del cálculo de Schubert cuántico en variedades de banderas afines requiere el uso de "vecindades de curvas combinatorias". En el caso específico del tipo $A_1^{(1)}$ , estas vecindades pueden codificarse mediante el grafo de momentos del grupo diedral infinito $D_\infty$ . Aunque existen fórmulas explícitas para estas vecindades (propuestas por Mihalcea y Norton), sus demostraciones implican pasos combinatorios complejos —como la verificación de paridad y longitudes de palabras— que son susceptibles a errores humanos. El problema central es la necesidad de una verificación formal y rigurosa de estas estructuras algebraicas y combinatorias.

Metodología
Los autores emplean el asistente de pruebas Lean 4 y la biblioteca matemática Mathlib para realizar una formalización "libre de axiomas". La metodología se divide en varios niveles de abstracción:

Modelado de Grupos de Coxeter: En lugar de tratar a $D_\infty$ solo como un grupo geométrico, lo dotan de una instancia de CoxeterSystem. Esto permite utilizar la infraestructura abstracta de Mathlib para manejar longitudes de elementos y relaciones de reflexión.
Construcción de Funciones Computables: Dado que la longitud de un grupo de Coxeter suele definirse de forma no constructiva, los autores desarrollan una función explicit_length basada en palabras reducidas para permitir el cálculo directo.
Definición del Grafo de Momentos: Formalizan el grafo mediante predicados inductivos (HasIncreasingChain), donde las aristas están vinculadas a reflexiones de raíces y grados específicos.
Tratamiento de la Aritmética de Paridad: Para formalizar los lemas de paridad, traducen las restricciones geométricas a aritmética de Presburger en $\mathbb{N}$ , utilizando el táctico omega de Lean para resolver los objetivos de aritmética lineal de forma automática.

Contribuciones Clave

Formalización de $D_\infty$ como Sistema de Coxeter: Lograron una equivalencia multiplicativa (MulEquiv) entre la representación geométrica y la abstracta, permitiendo el uso de herramientas de teoría de grupos avanzadas.
Puente entre Teoría y Computación: Desarrollaron un método para transformar conjuntos definidos matemáticamente (que en Lean son puramente lógicos) en conjuntos finitos computables (Finset). Esto se logra mediante el establecimiento de cotas superiores de longitud basadas en el grado.
Verificación del Teorema Principal: Probaron formalmente que la vecindad de curva $\Gamma_d(u)$ coincide con el conjunto de elementos maximales en el conjunto algebraico $A_d(u)$ , validando la fórmula de Mihalcea y Norton.

Resultados

Demostración Mecánica: Se obtuvo una prueba verificada por máquina de la fórmula principal que rige las vecindades de curvas para el tipo $A_1^{(1)}$ .
Implementación Ejecutable: El sistema no solo demuestra teoremas, sino que es capaz de realizar cálculos simbólicos. Mediante el uso de #eval, los autores demostraron que el código puede reproducir instantáneamente los resultados de las fórmulas originales (por ejemplo, calculando vecindades para elementos específicos como $r(2)$ o $s_0$ ).

Significancia
Este trabajo es significativo por dos razones principales:

Rigor en el Cálculo de Schubert Cuántico: Proporciona una base sólida y libre de errores para investigadores que trabajan con variedades de banderas afines y grupos de Kac-Moody.
Integración de Prueba y Computación: Demuestra que Lean 4 puede servir tanto como un entorno de verificación de teoremas de alto nivel como una herramienta de computación algebraica, cerrando la brecha entre la intuición matemática informal y la ejecución algorítmica exacta.