Aquí presento una auto-formalización completa de un reciente artículo de matemáticas (¡otra vez!) Barańczuk, Stefan. "Reduciendo el número de ecuaciones que definen un subconjunto del n-espacio sobre un campo finito." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Pasé unos días en este proyecto. Primero, ejecuté Aristotle por @HarmonicMath, que en aproximadamente 15 horas formalizó completamente la prueba. Luego, con la gran ayuda de @PietroMonticone, logré establecer una versión de plano de la prueba. 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 prueba y estudiar sus relaciones. En la etapa de post-procesamiento, 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 prueba formal. Esto es de gran ayuda para las personas que no son programadores profesionales de Lean 4. Realmente puedes internalizar todos los pasos de la prueba. 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 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!

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