🔢 mathematics

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0

Este artículo presenta una formalización completa y sin disculpas del teorema de Stokes en Lean 4 para cubos singulares suaves mediante pullbacks verdaderos de formas diferenciales, estableciendo puentes con mathlib4, verificando propiedades a nivel de cadena como $d^2=0$ y comparando la implementación con la formalización de Harrison en HOL Light.

Autores originales: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

Publicado 2026-05-05

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

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 tienes una forma muy compleja y multidimensional, como un trozo de papel arrugado o una cinta retorcida flotando en el espacio. En matemáticas, existe una regla famosa llamada Teorema de Stokes. Piénsalo como una "regla contable" universal para las formas. Dice que si quieres conocer la "actividad" total que ocurre dentro de una forma (como el viento total que gira dentro de un tornado), no necesitas medir cada punto individual en su interior. En cambio, solo necesitas medir el "borde" o la "frontera" de esa forma. La suma de toda la actividad en el borde equivale perfectamente a la actividad total en el interior.

Durante mucho tiempo, las computadoras (específicamente un programa llamado Lean 4) no habían sido capaces de probar esta regla para cada forma posible, especialmente las extrañas y arrugadas que los matemáticos llaman "cubos singulares".

Este artículo es un informe sobre cómo tres investigadores finalmente enseñaron a la computadora a probar esta regla para esas formas complicadas, sin cometer errores ni saltarse pasos.

Aquí hay un desglose de lo que hicieron, usando analogías simples:

1. El Objetivo: La Regla de "Borde vs. Interior"

Imagina que estás pintando una habitación. El Teorema de Stokes es como un truco de magia que dice: "Si sabes exactamente cuánta pintura goteó de las paredes (la frontera), automáticamente sabes exactamente cuánta pintura se usó para cubrir toda la habitación (el interior)".

Los investigadores querían probar que este truco funciona incluso si la "habitación" es una forma extraña y estirada definida por un mapa suave y retorcido (como una lámina de goma siendo estirada y retorcida).

2. El Truco de Magia de Tres Pasos

La computadora no podía simplemente "ver" toda la forma de una vez, así que los investigadores dividieron la prueba en tres pasos lógicos, como una receta:

Paso 1: La "Traducción" (Pullback)
Imagina que tienes un mapa de una ciudad, pero la ciudad está distorsionada. Los investigadores crearon una herramienta para "traducir" las matemáticas desde la forma distorsionada de vuelta a un cubo perfecto y estándar (como un dado perfecto). Utilizaron una herramienta matemática específica llamada "pullback" (que es como una fotocopiadora de alta tecnología que copia las reglas de la forma sobre una cuadrícula estándar).
Paso 2: La Regla de la "Caja Estándar"
Una vez que la forma fue traducida a un cubo perfecto, pudieron usar una regla más simple y ya conocida que funciona para cajas perfectas. Probaron que la "actividad interior" en este cubo perfecto es igual a la "actividad en el borde" en el cubo perfecto.
Paso 3: La "Coincidencia de Caras"
Finalmente, tuvieron que probar que los bordes del cubo perfecto (la versión traducida) coincidían perfectamente con los bordes de la forma original y extraña. Mostraron que cuando sumas los bordes de la forma extraña, se cancelan entre sí y se alinean exactamente con los bordes del cubo perfecto.

3. La Conexión de la "Cadena"

Los investigadores no solo lo probaron para una sola forma. Lo probaron para toda una "cadena" de formas unidas.

La Analogía: Imagina construir un muro con ladrillos. Si pones dos ladrillos juntos, el borde donde se tocan desaparece porque está dentro del muro. Los investigadores probaron que si tienes una cadena de estas formas, los bordes "interiores" siempre se cancelan entre sí, dejando solo la frontera exterior. Esta es una regla fundamental en matemáticas llamada $\partial^2 = 0$ (la frontera de una frontera es nada). Lo probaron mostrando que por cada vez que aparece un borde, aparece dos veces con signos opuestos, borrándose efectivamente a sí mismo.

4. Por Qué Esto Importa (En el Mundo de la Computadora)

No se Permite "Lo Siento": En los sistemas de prueba por computadora, los programadores a veces escriben "lo siento" para decir: "Sé que esto es cierto, pero aún no lo he probado". Este artículo es especial porque tiene cero declaraciones de "lo siento". La computadora verificó cada paso individual y no encontró errores.
El Puente: Los investigadores construyeron un "puente" entre dos formas diferentes de hacer matemáticas en la computadora. Un método usa coordenadas simples (como una hoja de cálculo), y el otro usa definiciones abstractas y sofisticadas. Probaron que ambos métodos conducen a exactamente la misma respuesta, asegurando que la computadora no está simplemente adivinando.
Suavidad Real: Exigieron que las formas fueran "suaves globalmente", lo que significa que son perfectamente suaves en todas partes, no solo en el medio. Esto hizo que las matemáticas fueran más fáciles de manejar para la computadora, aunque es una regla más estricta de lo que los humanos suelen necesitar.

5. Lo Que NO Es

El artículo es muy honesto sobre sus límites:

No prueba esto para cada forma posible en el universo (como una forma con una esquina afilada o un agujero que cambia de tamaño).
No trata con "variedades" (superficies curvas como la superficie de una esfera) de la manera completa y compleja en que los matemáticos lo hacen usualmente. Se adhiere a formas que pueden ser mapeadas desde un cubo estándar.
Es una prueba matemática, no un experimento de física. No predice el clima ni diseña puentes; simplemente prueba que las reglas lógicas del cálculo se sostienen cuando son verificadas por una computadora.

Resumen

En resumen, este artículo es una victoria para la precisión matemática. Los investigadores enseñaron a una computadora a verificar una regla de cálculo de 200 años de antigüedad para una amplia variedad de formas retorcidas y multidimensionales. Lo hicieron traduciendo el problema a una caja estándar, probando la regla allí y luego mostrando que la traducción era perfecta. El resultado es una prueba de "cero errores" de que la regla de "el interior es igual al borde" funciona, incluso para las formas suaves más complicadas que podamos imaginar.

Resumen Técnico: Teorema de Stokes para Cubos Singulares Suaves en Lean 4

Enunciado del Problema
A abril de 2026, el ecosistema de Lean 4 (específicamente mathlib4) carecía de una formalización completa del teorema de Stokes para formas diferenciales en variedades suaves con frontera o para cadenas singulares. Aunque mathlib4 poseía el teorema de la divergencia para cajas alineadas con los ejes y una derivada exterior abstracta (extDeriv), aún no proporcionaba un teorema que integrara el pullback de una forma diferencial sobre un cubo singular suave (un mapa suave desde un cubo unitario hacia un espacio euclídeo arbitrario) y lo igualara a la suma alternada de integrales sobre las caras de la frontera. Las formalizaciones existentes, como el trabajo de Harrison en HOL Light, cubrían dominios convexos y poliedrales, pero no abordaban parametrizaciones singulares suaves ni la infraestructura específica del álgebra exterior abstracta de mathlib4.

Metodología
Los autores presentan una formalización "sin sorry" (cero suposiciones no demostradas) que cierra la brecha entre la integración basada en coordenadas y la geometría diferencial abstracta. El desarrollo se basa en tres pilares metodológicos principales:

Pullback Real mediante Derivada de Fréchet: La construcción central define el pullback de una forma diferencial $\sigma^*\omega$ utilizando la derivada de Fréchet (fderiv) de un mapa globalmente $C^\infty$ $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ . A diferencia de una simple precomposición de coeficientes, esta definición aplica la forma en el punto imagen $\sigma(x)$ a los vectores empujados hacia adelante por $D\sigma(x)$ , adheriéndose a las definiciones estándar de la geometría diferencial.
Reducción al Stokes de Caja: La estrategia de prueba reduce el caso singular al caso de caja alineada con los ejes. Al aprovechar el teorema extDeriv_pullback de mathlib4, los autores establecen la identidad de naturalidad $d(\sigma^*\omega) = \sigma^*(d\omega)$ . Esto permite aplicar el teorema de Stokes de caja existente (derivado del teorema de la divergencia de mathlib4) a la forma pullback $\sigma^*\omega$ sobre el dominio de parámetros $[0,1]^{n+1}$ .
Ajuste de Caras y Álgebra a Nivel de Cadena: Un componente técnico crítico es la "identidad de ajuste de caras", que demuestra que la integral de la forma pullback sobre una cara de la frontera de una caja corresponde exactamente a la integral de la forma sobre la cara singular correspondiente. Además, los autores formalizan la identidad de complejo de cadenas $\partial(\partial\sigma) = 0$ para cadenas singulares. Esto se logra no definiendo un homomorfismo de frontera en cajas sin decorar, sino construyendo una involución sin puntos fijos y que invierte el signo sobre el conjunto de índices de doble frontera, demostrando que los términos emparejados se cancelan algebraicamente.

Contribuciones Clave
El artículo presenta una formalización exhaustiva compuesta por 44 módulos Lean (aproximadamente 4.000 líneas) con 205 declaraciones nombradas. Las contribuciones específicas incluyen:

Teorema de Stokes Singular: Un teorema que establece que para cualquier mapa globalmente $C^\infty$ $\sigma: \mathbb{R}^{n+1} \to \mathbb{R}^m$ y cualquier $n$ -forma $C^\infty$ $\omega$ , la integral de $\sigma^*(d\omega)$ sobre el cubo unitario es igual a la suma alternada de las integrales de $\sigma^*\omega$ sobre las $2(n+1)$ caras.
Teorema Puente: Una prueba formal que valida que la derivada exterior basada en coordenadas de los autores (extDerivCoord) es consistente con la extDeriv abstracta de mathlib4 cuando se evalúa sobre vectores de la base estándar. Esto asegura que la implementación basada en coordenadas es matemáticamente sólida en relación con la API abstracta de la biblioteca.
Extensiones a Nivel de Cadena: La extensión del teorema de Stokes a combinaciones lineales formales $\mathbb{Z}$ de cubos singulares (cadenas singulares) mediante linealidad.
Prueba de $\partial^2 = 0$ : Una prueba formal de la identidad de complejo de cadenas $\partial(\partial\sigma) = 0$ para cadenas singulares, utilizando una involución combinatoria sobre el conjunto de índices de doble cara.
Especializaciones Dimensionales: Instanciaciones directas del teorema principal que recuperan el Teorema Fundamental del Cálculo (TFC), el Teorema de Green, el Teorema de la Divergencia y el Teorema de Gauss en 3D, así como la integración por partes y la regla de Leibniz.
Auditoría de Axiomas: Verificación de que todo el desarrollo depende únicamente de los tres axiomas estándar de Lean 4 (propext, Classical.choice, Quot.sound), confirmado mediante 79 verificaciones sistemáticas con #print axioms.

Resultados y Alcance
La formalización demuestra exitosamente el teorema de Stokes para:

Cubos Singulares Suaves: Mapas $\sigma$ que son globalmente suaves en $\mathbb{R}^{n+1}$ , integrados sobre el cubo de parámetros $[0,1]^{n+1}$ .
Cajas Alineadas con los Ejes: $n$ -formas coordenadas sobre cajas $[a,b] \subset \mathbb{R}^{n+1}$ .

El artículo señala explícitamente las siguientes limitaciones y fronteras de alcance:

Sin Teoría de Variedades: El dominio de integración es estrictamente el cubo de parámetros o una caja. El trabajo no formaliza la integración sobre variedades suaves generales, ni utiliza particiones de la unidad, cartas o atlas.
Suavidad Global: Los mapas singulares deben ser $C^\infty$ en todo $\mathbb{R}^{n+1}$ , una condición más fuerte que la suavidad en el cubo cerrado únicamente. Esta elección se hizo para simplificar la formalización evitando argumentos de regularidad de frontera y asegurando que la derivada de Fréchet esté bien definida en todas partes.
Sin Semántica de Dominio Imagen: El teorema trata la integral como una operación sobre el dominio de parámetros. No demuestra que la imagen de $\sigma$ constituya una subvariedad o una cadena geométrica orientada en el espacio objetivo.

Significado y Afirmaciones
Los autores afirman que este trabajo proporciona la primera formalización completa en Lean 4 del teorema de Stokes para cubos singulares suaves con un pullback de "verdadera" forma diferencial. Su importancia radica en:

Puente entre Concreto y Abstracto: El patrón del "teorema puente" valida una implementación concreta basada en coordenadas frente a la derivada exterior abstracta de mathlib4, ofreciendo una metodología reutilizable para futuras formalizaciones.
Reutilización de Infraestructura: El desarrollo depende en gran medida de la infraestructura existente de mathlib4 (teorema de la divergencia, extDeriv_pullback), demostrando cómo componentes de alto nivel de la biblioteca pueden componerse para demostrar teoremas geométricos complejos sin reinventar el análisis fundamental.
Complementariedad: El trabajo es complementario a la formalización en HOL Light de Harrison. Mientras que Harrison cubre dominios convexos/poliedrales con integración de gauge, este trabajo cubre parametrizaciones singulares suaves utilizando integración de Bochner y la API de geometría diferencial de mathlib4.
Preparación Fundamental: Al probar $\partial^2=0$ y establecer el teorema de Stokes a nivel de cadena, los autores proporcionan un bloque de construcción local necesario para una futura formalización completa del teorema de Stokes en variedades suaves con frontera, una vez que maduren las APIs de integración y orientación de variedades de mathlib4.

El artículo concluye que, aunque no resuelve el problema de la integración en variedades generales, establece la capa crítica de "cadena cúbica" con pullbacks reales, sirviendo como una base verificada para futuras extensiones.