💻 computer science

Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda

Este artículo presenta una formalización de la construcción de los números reales de Cauchy en la Teoría de Tipos de Homotopía dentro de Cubical Agda, demostrando que este enfoque evita la elección numerable, la sobrecarga de setoides y los problemas de seguimiento de niveles de universo inherentes a otras definiciones constructivas, al tiempo que se verifica de tipo sin postulados.

Autores originales: Jackson Brough

Publicado 2026-04-29

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Jackson Brough

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 que estás intentando construir una regla perfecta e infinita para medir todo en el universo. En el mundo de las matemáticas clásicas, esta regla es fácil de describir: simplemente tomas todas las posibles mediciones "aproximadas" (como 3.1, 3.14, 3.141, etc.) y dices: "Si dos secuencias de mediciones se acercan cada vez más entre sí, representan el mismo punto en la regla".

Sin embargo, en las Matemáticas Constructivas—un estilo de matemáticas que insiste en que debes poder realmente construir o computar la cosa de la que estás hablando—este enfoque sencillo choca contra un muro. Para probar que tu regla está completa, tienes que hacer una elección mágica: tienes que seleccionar una medición específica de una lista infinita de opciones para representar el punto final. Las matemáticas constructivas dicen: "Nada de magia. Si no puedes mostrarme cómo lo elegiste, aún no has construido la regla".

Durante décadas, los matemáticos tuvieron que comprometerse. O bien usaban trucos de "contabilidad" que hacían cada cálculo desordenado, o bien construían la regla de una manera que requería rastrear complejos "niveles de universo" (como llevar la puntuación de qué tan grandes son tus cajas).

El Nuevo Plano (Reales del Libro HoTT)
Esta tesis presenta un nuevo plano para construir la regla, tomado del famoso libro Homotopy Type Theory (HoTT). En lugar de construir la regla pegando piezas y luego intentando alisarlas, este método construye la regla y las reglas de "suavidad" simultáneamente.

Piénsalo como construir una casa donde las paredes y el plano se están dibujando al mismo tiempo exacto.

Los Ladrillos: Comienzas con números simples y conocidos (como fracciones).
El Pegamento: Añades una regla especial que dice: "Si dos puntos están lo suficientemente cerca, en realidad son el mismo punto".
La Magia: Debido a que la regla de "proximidad" está integrada en la definición de la casa misma, no necesitas hacer esas elecciones mágicas más tarde. La casa está completa en el momento en que terminas de colocar los ladrillos.

El Desafío: El Traductor Computacional
El autor, Jackson Brough, tomó este plano teórico e intentó traducirlo a un lenguaje que una computadora pueda entender y verificar: Cubical Agda.

Imagina intentar explicar una rutina de baile compleja a un robot que solo entiende instrucciones estrictas y literales.

El Problema: Los intentos anteriores de traducir este plano fallaron porque el lenguaje de la computadora no tenía los "movimientos" adecuados (específicamente, no podía manejar la definición simultánea de la regla y las reglas de proximidad). Los traductores tenían que decir: "Asume que este movimiento existe", lo cual es hacer trampa en matemáticas.
La Solución: Cubical Agda es un robot más nuevo y más inteligente que nativamente entiende estos movimientos complejos. Permite al autor escribir el plano exactamente como fue diseñado, sin hacer trampa.

Qué Sucedió Durante la Traducción
La tesis no se trata solo de escribir código; se trata de lo que sucedió cuando el autor intentó hacer que la computadora entendiera las matemáticas. La estricta rigurosidad de la computadora obligó al autor a encontrar brechas ocultas en la explicación original:

El Mapa "Alternativo": El libro original describía cómo verificar si dos puntos están cerca. Pero cuando el autor intentó escribir el código, se dio cuenta de que el método del libro era como una "calle de un solo sentido". Podías probar que los puntos estaban cerca, pero no podías trabajar fácilmente hacia atrás para ver por qué. El autor tuvo que construir un segundo mapa "computacional" (llamado relación alternativa) que actúa como una marcha atrás, permitiendo que la computadora realmente calcule la respuesta.
El Ingrediente Faltante: El libro describía una regla para construir funciones (como la multiplicación) como si la computadora pudiera "recordar" la lista original de aproximaciones. La primera versión del código del autor olvidó esta memoria. La computadora la rechazó. El autor tuvo que reescribir la regla para llevar explícitamente la memoria consigo, dándose cuenta de que el texto original había sido demasiado vago para una máquina.
El Rompecabezas de Múltiples Variables: El libro insinuaba que las reglas para números individuales podían aplicarse fácilmente a pares o tríos de números. La computadora no estaba convencida. El autor tuvo que probar un nuevo lema específico que mostraba que si una regla funciona para una variable, funciona para dos, siempre que las verifiques una a la vez.

El Resultado
El producto final es una biblioteca masiva de código de código abierto (con más de 13,000 líneas) que prueba que los reales del libro HoTT funcionan perfectamente.

Prueba que estos números forman un campo ordenado completo (puedes sumar, restar, multiplicar, dividir y compararlos).
Prueba que la regla es "Arquimediana" (lo que significa que no importa cuán pequeño sea un hueco que tengas, siempre puedes encontrar una fracción que quepa dentro de él).
Lo más importante, hace todo esto sin hacer trampa. La computadora verificó cada paso individual, y el código se ejecuta sin ninguna "asunción mágica".

En Resumen
Esta tesis es la historia de tomar una idea matemática hermosa y de alto nivel y obligarla a sobrevivir en el mundo riguroso y literal de la verificación computacional. Al hacerlo, el autor no solo construyó una regla digital; pulió el propio plano, revelando detalles ocultos y haciendo la teoría más fuerte y precisa de lo que era antes. El código ahora está disponible para que cualquiera lo utilice como una base sólida para futuros descubrimientos matemáticos.

Aquí se presenta un resumen técnico detallado de la tesis "Formalizando los Números Reales en Teoría de Tipos de Homotopía con Cubical Agda" de Jackson Brough.

1. Planteamiento del Problema

Las matemáticas constructivas buscan proporcionar interpretaciones computacionales para las pruebas matemáticas, pero la construcción de los números reales ( $\mathbb{R}$ ) ha requerido históricamente compromisos significativos:

Construcción Clásica de Cauchy: Requiere el Axioma de Elección Numerable para seleccionar representantes de las clases de equivalencia de sucesiones de Cauchy y probar la completitud de Cauchy. Esto es no constructivo.
Construcción de Setoides de Bishop: Evita la elección trabajando con sucesiones de Cauchy equipadas con una relación de equivalencia explícita (setoides). Sin embargo, esto introduce una sobrecarga de gestión persistente, requiriendo pruebas de congruencia explícitas para cada operación y teorema, lo que complica las estructuras algebraicas.
Cortes de Dedekind: En la teoría de tipos predicativa, los cortes de Dedekind requieren rastrear niveles de universo (los reales viven un nivel por encima de sus cortes), lo que hace que los desarrollos sean engorrosos.

El Libro HoTT (Teoría de Tipos de Homotopía) propone una solución: definir los números reales como un Tipo Inductivo-Inductivo Superior (HIIT). Esta construcción evita la elección, elimina la sobrecarga de setoides al identificar reales $\epsilon$ -cercanos mediante constructores de caminos, y evita el rastreo de niveles de universo. Sin embargo, formalizaciones anteriores (por ejemplo, de Gilbert en Rocq) estaban incompletas porque los asistentes de prueba carecían de soporte nativo para HIITs, obligando al autor a postular los constructores de caminos y sus reglas de computación en lugar de derivarlos.

2. Metodología

La tesis presenta una formalización completa y verificada por máquina de los reales del libro HoTT utilizando Cubical Agda, un asistente de pruebas basado en la Teoría de Tipos Cúbica.

Soporte Nativo: Cubical Agda soporta nativamente Tipos Inductivos Superiores (HITs) y definiciones Inductivo-Inductivas. Esto permite al autor definir los reales y la relación de cercanía simultáneamente sin postulados, asegurando que los constructores de caminos tengan reglas de computación nativas.
Alcance de la Formalización: El trabajo formaliza más de 13,000 líneas de código, cubriendo:
1. La definición HIIT de $\mathbb{R}$ y la relación de cercanía ( $\sim_\epsilon$ ).
2. Principios de inducción y recursión.
3. Propiedades de la relación de cercanía (reflexividad, simetría, desigualdad triangular, redondez).
4. Principios de extensión para aplicaciones de Lipschitz y no expansivas.
5. La construcción de operaciones algebraicas (suma, negación, min/max, multiplicación, recíproco).
6. Teoría del orden (desigualdades estrictas/no estrictas, separación).
7. La prueba de que $\mathbb{R}$ forma un cuerpo ordenado arquimediano.
Herramientas: El autor utilizó Claude Code (agente de IA de Anthropic) para ayudar a navegar la gran biblioteca estándar de Cubical Agda y convertir bocetos de pruebas informales en términos Agda formales, acelerando significativamente el desarrollo de pruebas complejas como la construcción del recíproco.

3. Contribuciones Clave

A. La Primera Formalización Completa de los Reales HoTT

Esta es la primera formalización de los reales del libro HoTT que no depende de postulados. Los intentos anteriores debían asumir la existencia de constructores de caminos; este trabajo los deriva directamente de la teoría de tipos de Cubical Agda, asegurando que todas las reglas de computación se cumplan definicionalmente.

B. Resolución de Brechas de Formalización

El proceso de formalización reveló problemas sutiles en la presentación informal del libro HoTT que requirieron refinamiento matemático:

Relación de Cercanía Alternativa: La definición inductiva de cercanía ( $\sim$ ) proporciona condiciones suficientes pero no necesarias para extraer testigos. La formalización construye rigurosamente una relación auxiliar ( $\approx$ ) que computa sobre constructores y prueba $\sim \iff \approx$ , permitiendo el análisis de casos sobre hipótesis de cercanía.
Principio de Recursión Mejorado: La notación del texto informal para el principio de recursión asumía tácitamente el acceso a la aproximación del dominio ( $x_\epsilon$ ) dentro de la hipótesis inductiva. La formalización requirió reformular explícitamente el principio de recursión para llevar tanto la aproximación como la asignación del codominio, un detalle pasado por alto en transcripciones iniciales ingenuas.
Continuidad Multivariable: El libro HoTT implica que la continuidad separada es suficiente para extender identidades a múltiples variables. La formalización probó esto explícitamente (Lema 2.3.4), mostrando que la continuidad separada es suficiente para extender identidades binarias y ternarias de $\mathbb{Q}$ a $\mathbb{R}$ .

C. Construcción de Multiplicación y Recíproco

La multiplicación y el recíproco no son globalmente Lipschitz, por lo que no pueden definirse mediante principios de extensión simples. La tesis adopta la estrategia de local a global de Gilbert:

Definir operaciones en dominios restringidos donde existen cotas de Lipschitz (por ejemplo, fijando una cota en un factor).
Probar que estas definiciones locales coinciden en las intersecciones.
Utilizar el Teorema de Kraus (aplicaciones desde truncamientos proposicionales a conjuntos) para eliminar la dependencia de la cota específica, obteniendo una definición global.
Este enfoque se implementó utilizando el módulo SetElim de la biblioteca estándar de Cubical Agda.

D. Eficiencia Computacional

A diferencia de la construcción de cociente clásica en Lean (donde $2+2=4$ en reales no es definicionalmente cierto), la construcción HoTT en Cubical Agda permite que la aritmética en entradas racionales computa definicionalmente. Por ejemplo, rational(2) + rational(2) = rational(4) se reduce a refl (reflexividad) directamente en el verificador de tipos.

4. Resultados

Cuerpo Ordenado Arquimediano: La formalización prueba exitosamente que el tipo construido $\mathbb{R}$ satisface todos los axiomas de un cuerpo ordenado arquimediano, incluida la existencia de inversos para elementos separados de cero.
Disponibilidad del Código: Toda la base de código (aproximadamente 13,500 líneas) es de código abierto y verifica tipos sin huecos ni postulados utilizando la última biblioteca estándar de Cubical Agda.
Desarrollo Asistido por IA: La tesis demuestra la eficacia del uso de agentes de codificación basados en LLM para matemáticas formales, específicamente para navegar bibliotecas grandes y traducir estrategias de prueba de alto nivel a términos de tipos dependientes de bajo nivel.

5. Significado

Fundacional para el Análisis Constructivo: Este trabajo proporciona una base robusta y verificada por máquina para el análisis constructivo dentro del programa de Fundamentos Univalentes. Elimina la carga de "gestión" de los setoides y la carga de "elección" de los cocientes clásicos.
Evolución de los Asistentes de Prueba: Valida Cubical Agda como un entorno superior para matemáticas basadas en HIIT en comparación con sistemas como Rocq (Coq) que carecen de soporte nativo para HITs.
Trabajo Futuro: La formalización prepara el escenario para extender el análisis constructivo a estructuras más complejas (por ejemplo, integración de Riemann, ecuaciones diferenciales) y generalizar conceptos como localizadores (estructuras que permiten computación en reales) a espacios métricos más amplios.
Perspectiva Metodológica: La tesis destaca que la formalización no es meramente un ejercicio de verificación, sino una actividad matemática que puede descubrir suposiciones implícitas y refinar teoremas de maneras que la lectura informal por sí sola no puede.

En resumen, la tesis de Jackson Brough cierra la brecha entre la elegancia teórica de los números reales del libro HoTT y las matemáticas prácticas y ejecutables, proporcionando una base verificada, computacionalmente eficiente y libre de postulados para el análisis real en la teoría de tipos.