2026-05-30
Context
In the domain of formal mathematical proofs and interactive theorem proving, Lean 4 and its standard mathematical library, mathlib4, represent a cornerstone for the mathematical community. However, the structural complexity and massive scale of interconnected mathematical declarations make understanding the web of dependencies between theorems, lemmas, and definitions a highly challenging task.
To address this challenge and assist mathematical research and learning, the Mathematical Dependency Interface was created—a lightweight, high-performance web-based 3D visualization tool designed to map, filter, and intuitively explore the logical dependencies within mathlib4.
2026-01-27
Context
The CineMX Yearbook of the Mexican Institute of Cinematography (IMCINE) constituted one of the most valuable public resources to audit, study, and research the state of cinema in Mexico. In late September 2025, I carried out an exhaustive data extraction (web scraping) process of the site in order to analyze thematic trends in Mexican films.
On January 27, 2026, the official online platform that allowed interactive query of these historical files was unexpectedly taken down. In order to prevent the loss of this historical information and encourage cultural and public data analysis, I decided to consolidate and open everything extracted through a public repository on GitHub.
2022-03-30
Context
Music has an innate ability to evoke complex emotional states. Studying how these emotions interact and overlap in large song catalogs is a highly interesting task for music recommendation systems.
In order to model and mathematically and visually understand the relationship between different moods, I developed Musical Moods Network, an interactive data science project that models the emotions of the MuSe (Multimodal Music Sentiment Analysis) dataset as a complex network of undirected graphs.