2026-05-30
Contexto
En el ámbito del desarrollo de pruebas matemáticas formales y el uso de asistentes de demostración, Lean 4 y su librería matemática estándar, mathlib4, desempeñan un papel central. Sin embargo, la complejidad estructural y el inmenso volumen de declaraciones interconectadas hacen que comprender las relaciones de dependencia entre teoremas, lemas y definiciones sea una tarea titánica.
Para abordar este desafío y facilitar la investigación matemática y el aprendizaje, se concibió el Mathematical Dependency Interface, una interfaz interactiva en 3D de alto rendimiento que permite mapear, filtrar y explorar visualmente las dependencias lógicas y teóricas de mathlib4.
2026-01-27
Contexto
El Anuario CineMX del Instituto Mexicano de Cinematografía (IMCINE) constituía uno de los recursos públicos más valiosos para auditar, estudiar e investigar el estado del cine en México. A finales de septiembre de 2025, realicé un proceso de raspado de datos (web scraping) exhaustivo del sitio con el fin de analizar tendencias temáticas en las películas mexicanas.
El 27 de enero de 2026, la plataforma en línea oficial que permitía la consulta interactiva de estas fichas históricas fue retirada de internet de forma imprevista. Con el fin de evitar la pérdida de esta información histórica y fomentar el análisis cultural y de datos públicos, decidí consolidar y abrir todo lo extraído mediante un repositorio público en GitHub.
2022-03-30
Contexto
La música tiene una capacidad innata para evocar estados emocionales complejos. Estudiar cómo interactúan y se solapan estas emociones en grandes catálogos de canciones es una tarea sumamente interesante para los sistemas de recomendación musical.
Con el fin de modelar y comprender de forma matemática y visual la relación entre los diferentes estados de ánimo, desarrollé Musical Moods Network, un proyecto interactivo de ciencia de datos que modela las emociones del dataset MuSe (Multimodal Music Sentiment Analysis) como una red compleja de grafos no orientados.