Mathematical Dependency Interface: Modelador 3D de Dependencias para Lean 4

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.