Auto-formalización con Aristóteles por @HarmonicMath y ingeniería inversa con @OpenAI GPT Codex CLI (en realidad GPT-5.2 con xhigh y todas las ventajas experimentales habilitadas). Trabajando en un ejercicio de Álgebra de Bourbaki sobre matrices, obtuve casi 900 líneas de código Lean 4 completamente documentado, incluyendo todos los detalles de la prueba. Luego lo pasé, utilizando una configuración agentica diseñada adecuadamente, a Codex CLI para realizar la ingeniería inversa del archivo LaTeX correspondiente, reconstruyendo los pasos de la prueba directamente desde Lean, al estilo de las pruebas estructuradas de Leslie Lamport. Esto aún no es el programa de Langlands, pero necesitamos que este tipo de matemáticas de nivel intermedio se automatice. Y esto está sucediendo ahora. Simplemente construí la configuración agentica correcta, encadené todo y extraje el texto de Bourbaki (incluso esa parte funcionó bien con @grok 4.1, que es genial para previsualizar LaTeX en vivo). Terminaré la documentación y la publicaré en GitHub. Revisa el gráfico de dependencias: Aristóteles lo manejó todo por sí mismo. Y la prueba es completamente interactiva. ¡Estamos viviendo en el futuro de la ciencia ahora!

En esta publicación de la comunidad quiero poner enlaces a algunos juegos y entornos interactivos muy atractivos (disponibles de forma gratuita) que ayudan a las personas a explorar conceptos sofisticados tanto en programación como en matemáticas. Si conoces algún otro lugar divertido para visitar, simplemente publica abajo. ¡Diviértete! Lean: Una colección de acertijos de programación muy atractivos que te ayudan a aprender cómo se prueban y formalizan las matemáticas. Nunca volverás a ver de la misma manera la dificultad de 5*7=7*5. NandGame: Crea tu propio procesador desde cero (incluso NAND se hace a partir de circuitos más simples). ¡Altamente adictivo y súper divertido! Quantum Flytrap: Aquí es donde finalmente obtendrás una comprensión de los cálculos cuánticos. Colorido, ilimitado, atractivo y matemáticamente muy profundo. Scratch: Aprende programación de manera divertida. Euclidea: Aprende a realizar construcciones con regla y compás. Solía ser parte de la educación escolar, pero ahora es una aplicación. Divertido y muy informativo. Planarity: Intenta encontrar una incrustación de grafo que demuestre que es efectivamente planar. Golly: El explorador definitivo de autómatas celulares. Si quieres profundizar: SageMath: Es un poderoso sistema de álgebra computacional con sintaxis de Python. Es ideal para cursos y la sintaxis de SageMath está mucho más cerca del discurso matemático regular. Me gusta enseñar cursos con SageMath. GeoGebra: Puedes hacer pruebas, cálculos y applets interactivos. Es una forma divertida de aprender muchas facetas diferentes de las matemáticas de pregrado. Wolfram Demonstration Projects: Una colección de applets matemáticos que pueden ayudarte a entender temas muy sofisticados. No necesitas Mathematica para ejecutarlos, pero lo necesitas para diseñar tus propios applets. The Mechanics of Proof (por Heather Macbeth): Es un libro con un repositorio interactivo en GitHub donde puedes aprender de manera más completa la estructura y sintaxis de Lean. An Illustrated Theory of Numbers (por Martin H. Weissman): Este es un libro de texto sobre teoría de números elemental con aplicaciones. Y estas aplicaciones están disponibles en el sitio web como una colección de Jupyter Notebooks gratuitos que te enseñan los conceptos clave. Graphical Linear Algebra: Una forma ilustrada y, hasta cierto punto, interactiva de aprender conceptos profundos en álgebra. HomotopyContinuation.jl: Esta es una forma increíblemente hermosa e interactiva (con Julia) de aprender algunas ideas altamente complejas de la geometría algebraica (componentes conectados, método de continuación de homotopía) y con aplicaciones a sistemas algebraicos muy especiales que provienen de aplicaciones. Puedes aprender Julia en el camino. Mathamaze: Es una experiencia de Helena Verrill. Geometría hermosa, mosaicos, patrones. Simplemente maravilloso. Difícil de explicar: n: el camino del ninja: Si piensas que las matemáticas son difíciles. Aprende la paciencia de la manera difícil. Advertencia: altamente adictivo. HyperRogue: Puedes aprender geometría hiperbólica en un entorno de tipo rogue.

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