Mathematical Dependency Interface: 3D Dependency Viewer for Lean 4

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.