Abstract:Dependency graphs that show how definitions, theorems, and proofs relate to each other are valuable for understanding the structure of mathematical texts. Existing tools such as Lean Blueprint and plasTeXdepgraph generate such graphs within formal proof ecosystems, but they require familiarity with proof assistants or specific compilation pipelines. We present KnowTeX, a standalone Python tool that extracts dependency graphs directly from LaTeX sources without requiring any external framework. KnowTeX supports two complementary modes: a manual mode where authors annotate their source with lightweight commands compatible with Lean Blueprint, and an infer mode that automatically discovers dependencies through a layered system of deterministic and heuristic rules. The tool handles multi-file projects, detects cycles, applies transitive reduction, and exports graphs in DOT, TikZ, and PNG formats with an interactive preview. We evaluate KnowTeX on several mathematical texts and discuss how it complements recent tools such as LeanArchitect, which operates from the Lean side, while KnowTeX works entirely on the LaTeX side without requiring any formalization.
From: Elif Uskuplu [view email]
[v1]
Tue, 16 Dec 2025 18:24:28 UTC (76 KB)
[v2]
Sat, 5 Sep 2026 22:18:48 UTC (787 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。