KnowTeX: Visualizing Mathematical Dependencies

TL;DR

KnowTeX is a user-friendly tool that visualizes mathematical dependencies directly from LaTeX sources, aiding understanding, education, and formalization of mathematical texts through generated dependency graphs.

Contribution

It introduces a simple method to extract and visualize dependencies in LaTeX documents, extending ideas from Lean's Blueprints for broader mathematical writing.

Findings

Enables visualization of mathematical dependencies from LaTeX sources

Supports educational and formalization efforts with dependency graphs

Proposes dependency graphs as a standard feature in mathematical writing

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.