用LaTeX生成数学定理依赖图，让抽象推导变可视化。
KnowTeX: Visualizing Mathematical Dependencies
- 通过LaTeX中的'uses'指令自动提取定理间依赖关系
- 生成可预览的DOT/TikZ格式依赖图，清晰展现推导脉络
- 适合数学教育、形式化证明与跨文本知识对齐
数学知识以非正式教材、讲义到大型形式化证明库等多种形式存在，但不同表示间转换困难。非正式文本隐藏依赖关系，而形式系统虽详尽却难读。依赖图提供了中间路径，使结果、定义和证明的结构可视化。我们提出KnowTeX，一个独立易用的工具，扩展Lean的Blueprints思想，可直接从LaTeX源码中提取概念依赖关系。通过简单的“uses”命令，KnowTeX能识别命题间的关联，并生成可预览的DOT和TikZ格式图形。应用于数学文本时，此类图表能阐明核心结论，支持教学与形式化，为非正式与形式化数学表达的对齐提供资源。我们认为，依赖图应成为数学写作的标准功能，惠及人类读者与自动化系统。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。