Terence Tao’s paper diagram visualizer turns a structured description of theorem dependencies into an interactive graph. Nodes can represent definitions, lemmas, propositions, or major proof stages; edges describe claimed dependencies; the result can be explored and exported to several diagram formats.
My original LinkedIn post described the tool too loosely as converting a hand-drawn sketch into a formal visualization. The actual workflow is more interesting: the visualizer consumes formatted JSON, while a person or an AI system constructs the dependency data. Separating extraction from presentation makes the tool deterministic, but it does not make the extracted mathematical structure automatically correct.
Why the representation is useful
Long mathematical papers rarely have a purely linear reading order. A theorem may depend on a small structural spine surrounded by technical estimates, alternative constructions, and background results. A dependency diagram can reveal:
- which definitions feed the main result;
- where several proof branches converge;
- which lemmas are reused across sections;
- which parts can be read independently;
- where an apparent proof shortcut omits an intermediate obligation.
This is valuable before formalization. It gives a reader a navigational model and gives an author a different view of the exposition. The graph can also support review by making a proposed logical structure explicit enough to challenge.
The epistemic limit
The diagram is only as reliable as its nodes and edges. Tao notes that the demonstration diagrams were generated with language models and spot-checked, not proved complete. That distinction matters.
An attractive graph can fail in several ways:
- an edge is missing because a dependency is implicit in prose;
- a model invents a dependency that sounds mathematically plausible;
- two results are connected at the level of topic rather than proof;
- a crucial assumption is represented as decoration rather than as a prerequisite;
- the graph preserves local references while missing a global circularity;
- a paper revision makes the extracted structure stale.
The visualizer therefore produces a map of a claimed proof structure, not a proof certificate. Visual clarity should not be confused with logical validation.
How to evaluate an extracted diagram
A useful research workflow would preserve provenance for every graph element:
- each node links to the exact theorem, definition, or passage it represents;
- each edge records the passage or formal reference that justifies the dependency;
- uncertain or model-inferred edges are visually distinct from author-declared ones;
- reviewers can mark missing, spurious, or ambiguous dependencies;
- the diagram is versioned with the paper from which it was extracted.
Evaluation should include both positive and negative questions. Does every declared reference appear in the graph? Does every graph edge have textual support? Are important assumptions represented? Can a reviewer identify edges that should not exist? Coverage without precision creates noise; precision without coverage creates a falsely simple proof.
Connection to an independent research notebook
For research in progress, the same representation can connect definitions, computational experiments, counterexamples, and formal claims. A failed experiment may invalidate an edge without invalidating the entire graph. A conjectural step can remain visible as conjectural. Code and data can be attached to the claim they actually support.
This is especially useful when a project moves from exploratory calculations toward a paper. The diagram can show where evidence exists and where an argument still depends on an unverified transition. Once parts are formalized in a proof assistant, verified dependencies could be distinguished from inferred ones.
Used this way, a paper diagram does not replace reading or proof checking. It makes the structure inspectable—and therefore easier to question.