KnowTeX: Visualizing Mathematical Dependencies
Elif Uskuplu, Lawrence S. Moss, Valeria de Paiva
TL;DR
Problem: navigating between informal mathematical texts and formal proofs is challenging. Approach: KnowTeX is a standalone Python tool that extracts conceptual and logical dependencies from LaTeX sources using explicit commands such as \\uses (and optional \\proves), producing DOT and TikZ graphs with transitive closure. Contributions: lightweight, LaTeX-native visualization, compatibility with Lean Blueprint and plasTeXdepgraph, and a pathway toward standardizing dependency graphs in mathematical writing. Significance: improves learning, planning for formalization, and corpus-driven analysis by making the structure of mathematical knowledge explicit and reusable.
Abstract
Mathematical knowledge exists in many forms, ranging from informal textbooks and lecture notes to large formal proof libraries, yet moving between these representations remains difficult. Informal texts hide dependencies, while formal systems expose every detail in ways that are not always human-readable. Dependency graphs offer a middle ground by making visible the structure of results, definitions, and proofs. We present KnowTeX, a standalone, user-friendly tool that extends the ideas of Lean's Blueprints, enabling the visualization of conceptual dependencies directly from LaTeX sources. Using a simple "uses" command, KnowTeX extracts relationships among statements and generates previewable graphs in DOT and TikZ formats. Applied to mathematical texts, such graphs clarify core results, support education and formalization, and provide a resource for aligning informal and formal mathematical representations. We argue that dependency graphs should become a standard feature of mathematical writing, benefiting both human readers and automated systems.