💻 computer science

From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4

Este artículo presenta una formalización en Lean 4 de la integral de Dirichlet y sus aplicaciones, incluyendo la fórmula de Lobachevsky, empleando una estrategia que utiliza la función sinc al cuadrado absolutamente integrable y la densidad de los polinomios de coseno para manejar rigurosamente la convergencia condicional y derivar diversas identidades de integrales trigonométricas.

Autores originales: Daniel Goldberg, Antoine Vinciguerra

Publicado 2026-08-27

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Daniel Goldberg, Antoine Vinciguerra

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

En el vasto paisaje de las matemáticas, existe un rincón tranquilo dedicado al estudio de cómo las cosas se acumulan con el tiempo, particularmente cuando estas oscilan de un lado a otro. Este es el reino del análisis real, donde los matemáticos examinan el comportamiento de funciones que cambian continuamente. Uno de los acertijos más famosos en este campo involucra una curva específica que sube y baja como una onda, haciéndose cada vez más pequeña a medida que se extiende hacia el infinito. La pregunta es sencilla de plantear pero difícil de resolver: si sumas el área bajo esta curva oscilante desde el principio mismo hasta el punto más lejano que puedas imaginar, ¿qué total obtienes? Durante más de un siglo, los matemáticos han conocido la respuesta, pero demostrarla de manera rigurosa sin cometer supuestos ocultos siempre ha sido una tarea delicada. Esto se debe a que la curva no se estabiliza lo suficientemente rápido como para que las reglas estándar de suma se apliquen directamente; depende de una cancelación precisa de áreas positivas y negativas para alcanzar una suma finita. Comprender este comportamiento es crucial no solo para la matemática pura, sino también para la tecnología que sustenta la comunicación moderna, ya que estos mismos patrones oscilantes se utilizan para reconstruir señales e imágenes a partir de datos brutos.

Recientemente, dos investigadores, Daniel Goldberg y Antoine Vinciguerra, decidieron abordar este problema clásico utilizando un programa informático diseñado para verificar pruebas matemáticas con absoluta certeza. No se limitaron a escribir la solución; construyeron un argumento lógico completo y paso a paso dentro de un sistema de software llamado Lean 4, que actúa como un auditor incansable que se niega a aceptar un solo paso a menos que esté justificado por las reglas de la lógica. Su objetivo era formalizar la integral de Dirichlet, el nombre dado al cálculo de esa área oscilante específica, y mostrar cómo se conecta con un conjunto más amplio de reglas para integrar funciones periódicas. El desafío que enfrentaron fue que la forma estándar en que las computadoras manejan los cálculos de área, conocida como la integral de Lebesgue, no puede procesar directamente esta curva en particular porque el tamaño total de sus oscilaciones es infinito, aunque el área neta sea finita. Para sortear esto, los investigadores tuvieron que encontrar un desvío ingenioso que evitara el problema del infinito y, aun así, condujera a la respuesta correcta.

En lugar de intentar forzar a la computadora a aceptar la curva oscilante original directamente, el equipo primero analizó una versión modificada de la misma donde la curva se elevaba al cuadrado. Esta versión al cuadrado se comporta de manera mucho más amable; su área total es finita y bien comportada, lo que permite a la computadora calcularla mediante métodos estándar. Los investigadores luego demostraron una relación específica entre el área bajo la curva oscilante original y el área bajo esta versión al cuadrado. Al calcular primero el área de la curva al cuadrado, pudieron transferir matemáticamente ese resultado de vuelta al problema original. Este enfoque les permitió evitar las dificultades de la convergencia condicional, donde el orden de la suma importa, y llegar al famoso resultado de que el área total es exactamente la mitad del número pi. Esto no fue una conjetura o una simulación; fue una prueba rigurosa de que el límite del área, a medida que el límite se desplaza cada vez más lejos, converge a este valor específico.

Habiendo resuelto el acertijo principal, el equipo utilizó sus nuevas herramientas para explorar qué más podía derivarse de él. Demostraron cómo esta integral actúa como un filtro que puede convertir una onda suave y continua en un salto brusco, similar a un escalón, un comportamiento que es fundamental para el procesamiento de señales digitales. También descubrieron y demostraron una colección de otras identidades que involucran productos de estas funciones oscilantes, mostrando cómo diferentes frecuencias interactúan cuando se multiplican entre sí. Estos resultados no son meras curiosidades abstractas; proporcionan la base matemática para comprender cómo las señales pueden reconstruirse a partir de muestras, un concepto central en el teorema de muestreo de Shannon utilizado en el procesamiento de audio e imágenes digitales. Los investigadores demostraron que, al comprender el comportamiento de estas integrales específicas, uno puede derivar fórmulas precisas sobre cómo los diferentes patrones de ondas se combinan y se cancelan entre sí.

El logro final y quizás el más sorprendente de su trabajo fue la formalización de una fórmula descubierta por Nikolai Lobachevsky, un matemático conocido principalmente por su trabajo en la geometría no euclidiana. Lobachevsky había encontrado una regla que permite que el área bajo una curva oscilante multiplicada por un patrón repetitivo se calcule observando solo una pequeña sección de dicho patrón. Los investigadores demostraron que esta regla es válida para cualquier función continua y repetitiva que posea un tipo específico de simetría, utilizando la computadora para verificar que la suma infinita de las oscilaciones puede reducirse a un cálculo simple sobre un intervalo corto. Lo lograron demostrando que cualquier función repetitiva de este tipo puede aproximarse estrechamente mediante una suma de ondas de coseno simples, y dado que la regla funciona para cada onda individual, debe funcionar para la función completa. Esto proporciona una prueba verificada por máquina de una identidad general que anteriormente solo se había comprendido mediante la intuición humana y los métodos tradicionales de papel y lápiz.

El trabajo de Goldberg y Vinciguerra demuestra que incluso las verdades matemáticas centenarias pueden beneficiarse de la precisión de la verificación informática moderna. Al descomponer el problema en piezas manejables y navegar alrededor de los obstáculos que confunden los métodos de integración estándar, han creado una base sólida para la investigación futura en el procesamiento de señales y el análisis armónico. Su formalización confirma que la integral de Dirichlet es, de hecho, el límite de las áreas sobre intervalos acotados, y establece un marco fiable para la fórmula de Lobachevsky. Este logro sugiere que enfoques igualmente rigurosos podrían aplicarse a versiones más complejas de estas integrales, lo que potencialmente conduciría a nuevos hallazgos en nuestra comprensión de las estructuras matemáticas que gobiernan el mundo físico. El artículo es un testimonio del poder de combinar la profunda visión matemática con la lógica implacable de la verificación por computadora, convirtiendo un acertijo clásico en un hecho verificado.

Resumen Técnico: De la Integral de Dirichlet a la Fórmula de Lobachevsky

Planteamiento del Problema
El artículo aborda la formalización de la integral de Dirichlet, $\lim_{T \to +\infty} \int_0^T \frac{\sin t}{t} dt = \frac{\pi}{2}$ , dentro del asistente de pruebas Lean 4 utilizando la biblioteca Mathlib. El desafío principal radica en la naturaleza del integrando, la función $\text{sinc}$ ( $\sin t / t$ ), la cual no es integrable de Lebesgue en la semirrecta positiva porque no es absolutamente integrable. En la práctica matemática estándar, se utiliza laxamente la notación $\int_0^{+\infty} \text{sinc}(t) dt$ , pero en sistemas formales como Mathlib, la integral de Bochner de una función no integrableable se define como cero. En consecuencia, una formalización directa del valor de la integral es imposible; en su lugar, el problema debe plantearse como la convergencia de integrales truncadas. Además, las demostraciones clásicas que dependen del "truco de Feynman" (introducir un factor exponencial $e^{-at}$ y tomar el límite $a \to 0^+$ ) enfrentan obstrucciones formales: justificar el intercambio de límites requiere estimaciones de cola uniformes que son difíciles de coordinar dentro del marco formal de la convergencia condicional.

Metodología
Los autores adoptan una estrategia de prueba que evita las dificultades de la convergencia condicional mediante una ruta a través de la función $\text{sinc}^2$ , que es absolutamente integrable.

Evaluación de $\text{sinc}^2$ : La formalización establece primero que $\text{sinc}^2(t)$ es integrable de Lebesgue en $(0, \infty)$ . Evalúa la integral $\int_0^\infty \text{sinc}^2(t) dt$ introduciendo una función auxiliar $I(x) = \int_0^\infty e^{-xt} \text{sinc}^2(t) dt$ . Al derivar bajo el signo de la integral dos veces, los autores derivan una expresión de forma cerrada para $I(x)$ y toman el límite cuando $x \to 0^+$ utilizando el Teorema de la Convergencia Dominada (DCT), el cual es válido aquí porque $\text{sinc}^2$ es absolutamente integrable.
Recuperación de la Integral de Dirichlet: El valor de la integral de Dirichlet se recupera mediante una identidad que relaciona las integrales truncadas de $\text{sinc}$ y $\text{sinc}^2$ . Utilizando integración por partes, los autores demuestran que para cualquier $T > 0$ :
$\int_0^T \text{sinc}(t) dt = \int_0^{T/2} \text{sinc}^2(t) dt + \frac{T}{2}\text{sinc}^2\left(\frac{T}{2}\right)$
Cuando $T \to \infty$ , el término de frontera se anula, permitiendo que el límite de la integral de $\text{sinc}$ se iguale al límite de la integral de $\text{sinc}^2$ .
Estructura Formal: La formalización separa estrictamente los conceptos de integración de Lebesgue (usada para $\text{sinc}^2$ ) y el límite de integrales truncadas (usado para $\text{sinc}$ ). La convergencia se expresa utilizando los filtros Tendsto y atTop de Lean.

Contribuciones Clave y Resultados
El artículo presenta la formalización de tres familias interconectadas de resultados en análisis real:

La Integral de Dirichlet: Los autores proporcionan una prueba verificada por máquina de que el límite de las integrales truncadas de $\text{sinc}(t)$ converge a $\pi/2$ . Esto se logra sin invocar la integral de Lebesgue de la función no integrable en sí misma.
El Corte de Dirichlet y el Límite de Heaviside: La formalización deriva la convergencia de la primitiva normalizada $D(x) = \frac{1}{2} + \frac{1}{\pi}\int_0^x \text{sinc}(t) dt$ hacia la función de Heaviside. Específicamente, demuestra que $\lim_{R \to \infty} D(Rx) = H(x)$ puntualmente. Este resultado se extiende a una fórmula de corte integral, mostrando cómo $D(R(a-t))$ actúa como una identidad aproximada para funciones integrables.
Identidades de Integrales Trigonométricas: Utilizando la evaluación de la integral de $\textinc^2$ $\textinc2$ , los autores formalizan varias identidades cuadráticas y bilineales, incluyendo:
- $\int_0^\infty \left(\frac{\sin(at)}{t}\right)^2 dt = \frac{\pi |a|}{2}$
- $\int_0^\infty \frac{1-\cos(at)}{t^2} dt = \frac{\pi |a|}{2}$
- $\int_0^\infty \text{sinc}(at)\text{sinc}(bt) dt = \frac{\pi}{2 \max(a,b)}$
La Fórmula Integral de Lobachevsky: El artículo formaliza la fórmula de Lobachevsky para funciones periódicas continuas $f$ que satisfacen $f(x+\pi)=f(x)$ y $f(\pi-x)=f(x)$ . El teorema establece:
$\int_0^\infty \text{sinc}^2(x)f(x) dx = \int_0^{\pi/2} f(x) dx$
La demostración utiliza la densidad de los polinomios de coseno en el espacio de funciones continuas sobre el círculo aditivo $\mathbb{R}/\pi\mathbb{Z}$ (un resultado disponible en el análisis de Fourier de Mathlib). Los autores primero verifican la identidad para modos de coseno individuales y luego la extienden a funciones continuas generales mediante aproximación uniforme y un argumento de contradicción.

Significancia y Reivindicaciones
Los autores afirman que este trabajo proporciona la primera formalización de la fórmula integral de Lobachevsky en un asistente de pruebas. Si bien la integral de Dirichlet ha sido formalizada previamente en Isabelle/HOL (por Avigad et al.) utilizando un enfoque diferente basado en el teorema de Fubini y la representación de $1/x$ como una integral, la contribución de este artículo reside en su ruta específica a través de $\text{sinc}^2$ y su aplicación a la fórmula de Lobachevsky.

La significancia del trabajo es doble:

Metodológica: Demuestra una estrategia robusta para manejar integrales de convergencia condicional en sistemas formales, separándolas de sus contrapartes de convergencia absoluta, evitando así los problemas de la integración de Lebesgue directa para funciones no integrables.
Teórica: Une el análisis real clásico con las bibliotecas formales modernas al aplicar la infraestructura de análisis de Fourier de Mathlib (específicamente los resultados de densidad en el círculo aditivo) para probar una identidad de integral clásica que no había sido verificada por máquina anteriormente.

El artículo concluye señalando que la infraestructura desarrollada permite potenciales extensiones, tales como la formalización de fórmulas de tipo Lobachevsky para potencias pares superiores de la función sinc y aplicaciones a la teoría de la transformada de Laplace, aunque estas se presentan como direcciones futuras más que como trabajo completado.

Resumen Técnico: De la Integral de Dirichlet a la Fórmula de Lobachevsky

Más como este