← All papers
First page of KnowTeX: Visualizing Mathematical Dependencies

KnowTeX: Visualizing Mathematical Dependencies

Elif Uskuplu, Lawrence S. Moss, Valeria de Paiva

cs.HC Dec 16, 2025 · v1
Presents KnowTeX, a tool extending Lean's Blueprint system to generate mathematical dependency graphs from LaTeX sources.
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.

Mathematical knowledge has hidden dependency structures that are difficult to navigate in informal texts and overly detailed in formal systems, hampering both understanding and formalization efforts.

The authors present KnowTeX, a standalone tool that extends the ideas of Lean's Blueprints to visualize 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. It does not require a formal proof system.

Applied to mathematical texts such as Leinster's Basic Category Theory, KnowTeX produces dependency graphs that clarify core results and support education and formalization workflows.