Aquí presento una autoformalización completa de un trabajo reciente de matemáticas (¡otra vez!) Barańczuk, Stefan. "Reduciendo el número de ecuaciones que definen un subconjunto del n-espacio sobre un cuerpo finito." Annales de la Faculté des sciences de Toulouse : Mathématiques, serie, vol. 33, nº 1 (2024): 177–182. He dedicado unos días a este proyecto. Primero, ejecuté Aristóteles por @HarmonicMath , que en unas 15 horas formalizó completamente la demostración. Luego, con la gran ayuda de @PietroMonticone, conseguí configurar una versión plano de la demostración. Esta es una versión en la que todas las partes de la documentación en LaTeX se vuelven interactivas y pueden ser inspeccionadas y estudiadas. Podemos ver las dependencias en la demostración y estudiar sus relaciones. En la etapa de postprocesado, también utilicé Grok Heavy y Codex CLI con GPT-5.2 en modo xhigh para escribir un análisis línea por línea de la demostración formal. Esto es de gran ayuda para quienes no son programadores Lean 4 profesionales. Realmente puedes interiorizar todos los pasos de la demostración. Quiero resumir mis impresiones y lo que aprendí de esta experiencia. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

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!

Si fuera estudiante hoy, interactuar con LLMs de última generación sería casi como hacer trampa. Esta mañana hice una foto aleatoria de la pizarra y le pedí a ChatGPT-5.2-Pro que me explicara el contexto, la solución y algunos comentarios al margen sobre el famoso teorema de Chevalley sobre conjuntos constructibles. Lo que recibí fue un informe notablemente profundo, que sintetizaba material de alta calidad sobre geometría algebraica extraído de todo internet. Esto plantea una pregunta seria: ¿cuál es el verdadero esfuerzo y desafío para los estudiantes hoy en día? El coste es sin duda un factor, pero una vez que se dispone de acceso a estos modelos, ¿cómo se puede aprender en esta tierra de abundancia, donde explicaciones, referencias y exploración interactiva son instantáneamente accesibles? Quizá la lucha ya no sea obtener información o incluso entender argumentos individuales, sino desarrollar el juicio: saber qué preguntas hacer, qué explicaciones confiar, cómo reconocer la profundidad frente a la superficialidad plausible y cómo interiorizar las ideas en lugar de simplemente consumirlas. En un entorno donde las respuestas abundan, la verdadera dificultad puede estar en formar el gusto, la intuición matemática y la capacidad de navegar —en lugar de ahogarse— en este repentino exceso de conocimiento.