Los artículos matemáticos necesitan validación formal. Esto suele hacerse de forma informal por un árbitro. Pero, ¿y si pudiéramos confiar en algo más robusto como la autoformalización en Lean 4, donde el papel del revisor se reduciría a una revisión meticulosa de las formulaciones de definiciones y teoremas? La compilación de código generado automáticamente se convertiría en un certificado de prueba. Esto es lo que ocurrió en una etapa más larga que hice con Aristóteles de @HarmonicMath. Gracias a @PietroMonticone y @llllvvuu por ayudar con la configuración del plano. Aquí presento una autoformalización completa y correcta de un artículo de mi amigo Stefan Barańczuk sobre las secuencias divisibles de Chebyshev. El código consta de unas 5000 líneas de Lean altamente no trivial. Corrige todas las inconsistencias y lagunas en el artículo principal (incluso demostrando algunas proposiciones delegadas). Voy a publicar una serie de estos experimentos, demostrando que en algunas áreas de las matemáticas, incluyendo la teoría elemental de números, 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 demostraciones. ¡Creo que este va a ser un año caótico!