Los artículos matemáticos necesitan validación formal. Esto suele hacerse de manera informal por un árbitro. Pero, ¿y si pudiéramos confiar en algo más robusto como la auto-formalización en Lean 4, donde el papel del árbitro se reduciría a una verificación meticulosa de las formulaciones de las definiciones y teoremas? La compilación de código generado automáticamente se convertiría en un certificado de prueba. Esto es lo que sucedió en un proyecto más largo que hice con Aristóteles por @HarmonicMath. Gracias a @PietroMonticone y @llllvvuu por ayudar con la configuración del plano. Aquí presento una auto-formalización completa y correcta de un artículo de mi amigo Stefan Barańczuk sobre las secuencias de divisibilidad de Chebyshev. El código tiene unas 5000 líneas de Lean altamente no trivial. Corrige todas las inconsistencias y lagunas en el artículo principal (incluso probando algunas proposiciones delegadas). Voy a publicar una serie de tales experimentos, demostrando que en algunas áreas de las matemáticas, incluyendo la teoría de números elementales, la combinatoria y el análisis (todo tipo de cosas cubiertas por Mathlib), no estamos lejos de un cambio masivo en la documentación de la validez de las pruebas. ¡Creo que este va a ser un año agitado!