Auto-formalización con Aristotle por @HarmonicMath e ingeniería inversa con @OpenAI CLI del códex GPT (en realidad GPT-5.2 con xhigh y todas las ventajas experimentales activadas). 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 demostración. Luego lo aprobé —usando una configuración agential adecuadamente diseñada— para Codex CLI para hacer ingeniería inversa del archivo LaTeX correspondiente, reconstruyendo los pasos de demostración directamente desde Lean, al estilo de las demostraciones estructuradas de Leslie Lamport. Este aún no es el programa de Langlands, pero necesitamos que este tipo de matemáticas de nivel intermedio sean automatizadas. Y esto está ocurriendo ahora. Simplemente construí la configuración de agente adecuada, hice pipeline de todo y extraje el texto de Bourbaki (incluso esa parte funcionó bien con @grok 4.1, que es genial para previsualizar LaTeX en directo). Terminaré la documentación y la publicaré en GitHub. Revisa el grafo de dependencias: Aristóteles lo gestionó todo por sí solo. Y la demostración es totalmente interactiva. ¡Ahora vivimos en el futuro de la ciencia!

En esta publicación comunitaria quiero poner enlaces a algunos juegos y entornos interactivos muy atractivos (disponibles gratuitamente) que ayudan a la gente a explorar conceptos sofisticados tanto en programación como en matemáticas. Si conoces algún otro lugar divertido para visitar, simplemente publícalo abajo. ¡Que te diviertas! Esbelto: Una colección de acertijos de programación muy atractivos que te ayudan a aprender cómo se demuestran y formalizan las matemáticas. Ya no verás de la misma manera la dureza de 5*7=7*5. NandGame: Haces tu propio procesador desde cero (incluso la NAND está hecha con circuitos más simples). ¡Muy adictivo y súper divertido! Trampa cuántica: Aquí es donde finalmente entenderás las computaciones cuánticas. Colorido, ilimitado, atractivo y matemáticamente muy profundo. Scratch: Aprende a programar de la manera divertida. Euclidea: Aprende a hacer construcciones con regla y brújula. Antes formaba parte de la educación escolar, pero ahora es una aplicación. Divertido y muy informativo. Planaridad: Intenta encontrar una incrustación de grafo que muestre que es realmente planar. Vaya: El explorador definitivo de autómatas celulares. Si quieres profundizar más: SageMath: Es un potente sistema de álgebra computacional con sintaxis en Python. Es ideal para los cursos y la sintaxis de SageMath se acerca mucho más al discurso matemático habitual. Me gusta dar clases con SageMath. GeoGebra: Puedes hacer demostraciones, cálculos y applets interactivos. Es una forma divertida de aprender muchas facetas diferentes de las matemáticas de grado. Proyectos de demostración de Wolfram: Una colección de applets matemáticos que puede ayudarte a entender temas muy complejos. No necesitas Mathematica para ejecutarse, pero sí lo necesitas para diseñar tus propios applets. La mecánica de la demostración (por Heather Macbeth): Es un libro con un repositorio interactivo en GitHub donde puedes aprender de forma más completa la estructura y sintaxis de Lean. Una teoría ilustrada de los números (por Martin H. Weissman): Este es un libro de texto sobre teoría elemental de números con aplicaciones. Y estas aplicaciones están disponibles en la web como una colección de Cuadernos Jupyter gratuitos que te enseñan los conceptos clave. Álgebra Lineal Gráfica: De forma ilustrada y, en cierta medida, interactiva de aprender conceptos profundos en álgebra. HomotopyContinuation.jl: Esta es una forma increíblemente hermosa e interactiva (con Julia) de aprender ideas muy complejas desde la geometría algebraica (componentes conexos, método de continuación por homotopía) y con aplicaciones a sistemas algebraicos muy especiales que surgen de aplicaciones. Puedes aprender a Julia por el camino. Mathamaze: Es una experiencia de Helena Verrill. Geometría preciosa, mosaicos, patrones. Simplemente maravilloso. Difícil de explicar: N: El Camino del Ninja: Si crees que las matemáticas son difíciles. Aprende la paciencia por las malas. Aviso: altamente adictivo HiperPícaro: Puedes aprender geometría hiperbólica en un entorno tipo rogue-like.

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