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