A formalization of Borel determinacy in Lean

Este artículo presenta una formalización en Lean 4 de la determinación de Borel, que incluye la definición de juegos de Gale-Stewart y una prueba del teorema de Martin siguiendo su demostración puramente inductiva.

Lo esencial

Imagina que el universo de las matemáticas es un inmenso tablero de ajedrez infinito, donde dos jugadores, el "Blanco" y el "Negro", juegan una partida que nunca termina. En cada turno, eligen un movimiento de un conjunto de opciones. El juego continúa para siempre, generando una secuencia infinita de movimientos.

La pregunta clave es: ¿Alguien tiene una estrategia ganadora? Es decir, ¿puede uno de los jugadores planear sus movimientos de antemano de tal manera que, sin importar lo que haga el oponente, siempre termine ganando?

Este es el corazón de lo que se llama la determinación de juegos. En la mayoría de los casos, si el juego es simple (como un juego finito), sabemos que alguien siempre gana. Pero cuando los juegos se vuelven infinitos y las reglas de victoria son muy complejas (llamadas "conjuntos de Borel"), la cosa se pone muy difícil.

Aquí es donde entra este artículo, escrito por Sven Manthe, que es como un manual de construcción de un robot matemático llamado Lean.

¿Qué hizo el autor?

El autor tomó una prueba matemática muy famosa y difícil, descubierta por Donald Martin en los años 70, que dice: "En estos juegos infinitos complejos, siempre hay un ganador".

El problema es que la prueba de Martin es como un mapa escrito en un idioma antiguo y con muchas abreviaturas. Manthe decidió traducir ese mapa a un lenguaje que una computadora pueda entender y verificar paso a paso. Usó un programa llamado Lean 4, que actúa como un juez supremo y estricto: si un paso lógico tiene la más mínima duda, el juez grita "¡Error!" y no deja avanzar.

La analogía del "Desenredador"

Para entender cómo lo hizo, imagina que el juego es un ovillo de lana enredado.

• El problema: Quieres saber quién gana, pero el ovillo está tan enredado que no puedes ver el final.
• La solución de Martin: En lugar de intentar desenredar el ovillo de golpe, Martin sugirió usar una "máquina de desenredar" (llamada unraveling). Esta máquina transforma el juego original en un juego nuevo, más simple, donde las reglas de victoria son obvias (como un juego de "ganar o perder" inmediato).
• El truco: Si puedes demostrar que el juego nuevo es fácil de ganar, entonces el juego original también tiene un ganador.

Manthe tomó esta idea y la construyó pieza por pieza dentro de la computadora. Pero tuvo que hacer algunos ajustes creativos:

1. El problema de las "Listas Reversas": En matemáticas normales, a veces escribimos las listas de movimientos al revés de como las pensamos. Manthe decidió que, en su robot, las listas se escribirían de la forma natural (primero el primer movimiento, luego el segundo), para que fuera más fácil de leer.
2. El problema de las "Reglas de Oro": En la prueba original, Martin usaba un tipo de magia matemática llamada "inducción transfinita" (contar hasta números que no existen realmente). Manthe encontró una forma de evitar esa magia y usar un método más directo, como si construyera una escalera peldaño a peldaño en lugar de saltar al cielo.
3. El problema de los "Valores Basura": Aquí hay una discusión técnica muy interesante. Imagina que tienes una máquina que solo funciona si le das una manzana.
   • Enfoque tradicional (el que usa la mayoría de los matemáticos de Lean): Si le das una piedra, la máquina devuelve un "valor basura" (como un cero o un error) para que no se rompa. Es como decir: "Si no hay manzana, el resultado es 0".
   • El enfoque de Manthe: Él dijo: "No, si no hay manzana, la máquina simplemente no hace nada". En su código, las funciones solo existen donde tienen sentido. Esto es más fiel a cómo piensan los humanos, pero es mucho más difícil de programar porque la computadora se confunde si intentas hacer algo con un "nada". Manthe tuvo que enseñarle a su robot a manejar estos "vacíos" con mucho cuidado.

¿Por qué es importante esto?

Piensa en la matemática como un edificio. Durante décadas, hemos construido los cimientos (aritmética básica) y las paredes (álgebra, cálculo). Pero esta prueba de Martin es como el techo de cristal del edificio. Es una pieza de ingeniería tan compleja que, hasta ahora, nadie había logrado ponerla en un plano digital perfecto.

Al formalizarlo, Manthe ha logrado dos cosas:

1. Verificación absoluta: Ahora sabemos con un 100% de certeza, sin errores humanos, que la prueba de Martin es correcta. La computadora ha revisado cada línea.
2. Un nuevo lenguaje: Ha demostrado que podemos programar conceptos matemáticos muy abstractos sin tener que "hackear" el sistema usando trucos extraños (como los "valores basura").

En resumen

Este artículo es la historia de cómo un matemático tomó una prueba teórica muy elegante y complicada sobre juegos infinitos y la convirtió en un código de computadora que no miente ni se equivoca.

Es como si alguien hubiera tomado la receta secreta de un pastel imposible de hornear, la hubiera escrito en un libro de instrucciones para un robot de cocina, y el robot hubiera horneado el pastel perfecto, demostrando que la receta era correcta. Además, el robot aprendió a cocinar de una manera más limpia y natural que la que usaban los otros robots de la cocina.

Es un paso gigante para la matemática formalizada, donde la intuición humana se combina con la precisión infalible de la máquina.

Resumen técnico

Resumen Técnico: Formalización de la Determinación Boreliana en Lean

1. El Problema

La determinación de juegos infinitos es un tema central en la teoría descriptiva de conjuntos. Un juego de Gale-Stewart es determinado si uno de los dos jugadores posee una estrategia ganadora. Mientras que la determinación para clases grandes de conjuntos (como los analíticos) requiere axiomas de grandes cardinales, la determinación Boreliana (para conjuntos Borelianos) es demostrable dentro de la teoría de conjuntos ZFC estándar (teorema de Martin, 1975).

El desafío principal radica en la complejidad de la prueba original de Martin, que involucra inducción transfinita sobre la jerarquía Boreliana y construcciones de límites inversos de juegos. Formalizar esta prueba en un asistente de pruebas como Lean 4 presenta dificultades técnicas significativas:

• La necesidad de manejar funciones parciales y estrategias en posiciones específicas.
• La gestión de límites inversos de sistemas de árboles y la identificación de niveles estabilizados.
• La diferencia entre la teoría de tipos de Lean (basada en el Cálculo de Construcciones Inductivas) y la teoría de conjuntos ZFC, aunque ambas son consistentes en este contexto.

Hasta la fecha, no existía ninguna formalización de la determinación para clases de conjuntos más allá de los conjuntos cerrados en ningún asistente de pruebas.

2. Metodología

El autor formaliza la prueba siguiendo la presentación de Martin en su artículo de 1985 ("A purely inductive proof of Borel determinacy"), con adaptaciones necesarias para el entorno de Lean 4 y su biblioteca matemática (mathlib).

Enfoques Clave de la Formalización:

• Propiedad de "Desenredabilidad" (Unravelability): En lugar de probar la determinación directamente por inducción transfinita, el autor prueba una propiedad más fuerte llamada desenredabilidad universal.
  • Un juego es desenredable si para cada $k$, existe un $k$-recubrimiento que transforma el conjunto de pago en un conjunto abierto-cerrado (clopen).
  • Un juego es universalmente desenredable si su imagen bajo cualquier recubrimiento sigue siendo desenredable.
  • Se demuestra que los conjuntos universalmente desenredables forman un $\sigma$-álgebra, lo que permite evitar la inducción transfinita explícita sobre los ordinales, utilizando en su lugar inducción directa sobre la construcción de los conjuntos Borelianos.
• Estructura de Datos:
  • Las secuencias finitas se representan como listas (no se invirtieron, a diferencia de algunas convenciones en mathlib, para mantener la correspondencia directa con la notación matemática estándar).
  • Se definieron tres nociones de estrategia: estrategia funcional, cuasi-estrategia y pre-estrategia. La formalización priorizó las pre-estrategias (funciones de posiciones a conjuntos de movimientos, permitiendo conjuntos vacíos) por ser más fáciles de definir formalmente, aunque se usaron árboles de estrategia para definir la noción de "estrategia ganadora".
• Teoría de Categorías:
  • Se utilizó la biblioteca de teoría de categorías de mathlib para manejar los límites inversos necesarios para probar la estabilidad bajo uniones numerables.
  • Se definió una categoría $\mathcal{C}$ de árboles y morfismos. Se demostró que $\mathcal{C}$ tiene todos los límites y que el functor de restricción a niveles preserva estos límites, lo cual es crucial para la construcción del sistema inverso.
• Manejo de Funciones Parciales:
  • El proyecto adoptó el enfoque de funciones parciales mediante hipótesis proposicionales (tipos dependientes) en lugar de los "valores basura" (junk values) o elementos nulos que predomina en mathlib.
  • Ejemplo: Una estrategia se define como ∀x : T, IsPosition x.val p → Set (ExtensionsAt x), donde la función solo está definida si x es una posición válida del jugador p.

3. Contribuciones Clave

1. Primera Formalización de Determinación Boreliana: Es el primer trabajo que formaliza la determinación para cualquier clase de conjuntos más allá de los conjuntos cerrados en un asistente de pruebas.
2. Adaptación de la Prueba de Martin:
   • Se reemplazó la inducción transfinita por una inducción directa sobre la construcción Boreliana, introduciendo el concepto de desenredabilidad universal.
   • Se resolvió el problema de la estabilización de niveles en los límites inversos utilizando un lema de teoría de categorías en lugar de identificaciones ad-hoc.
3. Innovación en el Diseño de Funciones Parciales:
   • El autor argumenta y demuestra la viabilidad de usar tipos dependientes para funciones parciales en lugar de valores por defecto.
   • Se identificaron y solucionaron problemas de rendimiento (complejidad exponencial en el tiempo de ejecución) causados por la anidación de términos de prueba en tipos dependientes.
   • Se desarrolló un metaprograma (abstract) para abstraer automáticamente los términos de prueba en lemas auxiliares, mitigando el costo computacional.
4. Herramientas de Automatización:
   • Desarrollo de tácticas personalizadas para manejar aritmética de Presburger (paridad de longitudes de listas) y la inferencia automática de parámetros de "fijación" ($k$-fixing) en recubrimientos.

4. Resultados

• Código: El proyecto consta de aproximadamente 5,000 líneas de código en Lean 4.
• Estructura: Menos de la mitad del código cubre las definiciones fundamentales (juegos, determinación); la mayor parte formaliza la prueba de Martin, incluyendo la construcción de recubrimientos y la teoría de límites inversos.
• Validación: Se ha demostrado formalmente que todo juego Boreliano es determinado. La prueba sigue la lógica de Martin pero se ajusta a las restricciones y fortalezas de la teoría de tipos de Lean.
• Rendimiento: Se logró superar las barreras de rendimiento asociadas con el uso intensivo de tipos dependientes mediante la abstracción agresiva de términos de prueba.

5. Significado e Impacto

• Avance en Teoría Descriptiva: Este trabajo marca un hito al llevar resultados profundos de la teoría descriptiva de conjuntos (que históricamente han sido difíciles de formalizar debido a su complejidad lógica) al ámbito de la verificación formal.
• Validación de la Teoría de Tipos: Demuestra que la teoría de tipos de Lean, aunque ligeramente más fuerte que ZFC en términos de consistencia (equiconsistente con ZFC + cardinales inaccesibles), es capaz de formalizar teoremas que requieren fragmentos grandes de ZFC sin necesidad de axiomas adicionales.
• Debate Metodológico: El artículo ofrece una crítica constructiva a la convención de mathlib de usar "valores basura" para funciones parciales. El autor argumenta que el enfoque de tipos dependientes, aunque más desafiante para las tácticas de reescritura, refleja mejor las definiciones matemáticas informales y puede ser más robusto si se gestionan adecuadamente los problemas de rendimiento.
• Futuro: Abre la puerta a la formalización de determinación para clases más grandes (analíticas, proyectivas) bajo hipótesis de grandes cardinales y a la construcción de modelos internos en Lean.

En conclusión, el trabajo de Manthe no solo verifica un teorema fundamental de la matemática moderna, sino que también impulsa las capacidades de Lean 4 para manejar estructuras matemáticas complejas y debates sobre la mejor práctica de formalización de funciones parciales.