This is a somewhat experimental and speculative post. This week I was at the IPAM workshop on machine assisted proof that I was one of the organizers of. We had an interesting and diverse range of talks, both from computer scientists presenting the latest available tools to formally verify proofs or to automate various aspects of proof writing or proof discovery, as well as mathematicians who described their experiences using these tools to solve their research problems. One can find the videos of these talks on the IPAM youtube channel; I also posted about the talks during the event on my Mathstodon account. I am of course not the most objective person to judge, but from the feedback I received it seems that the conference was able to successfully achieve its aim of bringing together the different communities interested in this topic.

As a result of the conference I started thinking about what possible computer tools might now be developed that could be of broad use to mathematicians, particularly those who do not have prior expertise with the finer aspects of writing code or installing software. One idea that came to mind was a potential tool to could take, say, an arXiv preprint as input, and return some sort of diagram detailing the logical flow of the main theorems and lemmas in the paper. This is currently done by hand by authors in some, but not all, papers (and can often also be automatically generated from formally verified proofs, as seen for instance in the graphic accompanying the IPAM workshop, or this diagram generated from Massot’s blueprint software from a manually inputted set of theorems and dependencies as a precursor to formalization of a proof [thanks to Thomas Bloom for this example]). For instance, here is a diagram that my co-author Rachel Greenfeld and I drew for a recent paper:

This particular diagram incorporated a number of subjective design choices regarding layout, which results to be designated important enough to require a dedicated box (as opposed to being viewed as a mere tool to get from one box to another), and how to describe each of these results (and how to colour-code them). This is still a very human-intensive task (and my co-author and I went through several iterations of this particular diagram with much back-and-forth discussion until we were both satisfied). But I could see the possibility of creating an automatic tool that could provide an initial “first approximation” to such a diagram, which a human user could then modify as they see fit (perhaps using some convenient GUI interface, for instance some variant of the Quiver online tool for drawing commutative diagrams in LaTeX).

As a crude first attempt at automatically generating such a diagram, one couuld perhaps develop a tool to scrape a LaTeX file to locate all the instances of the theorem environment in the text (i.e., all the formally identified lemmas, corollaries, and so forth), and for each such theorem, locate a proof environment instance that looks like it is associated to that theorem (doing this with reasonable accuracy may require a small amount of machine learning, though perhaps one could just hope that proximity of the proof environment instance to the theorem environment instance suffices in many cases). Then identify all the references within that proof environment to other theorems to start building the tree of implications, which one could then depict in a diagram such as the above. Such an approach would likely miss many of the implications; for instance, because many lemmas might not be proven using a formal proof environment, but instead by some more free-flowing text discussion, or perhaps a one line justification such as “By combining Lemma 3.4 and Proposition 3.6, we conclude”. Also, some references to other results in the paper might not proceed by direct citation, but by more indirect justifications such as “invoking the previous lemma, we obtain” or “by repeating the arguments in Section 3, we have”. Still, even such a crude diagram might still be helpful, both as a starting point for authors to make an improved diagram, or for a student trying to understand a lengthy paper to get some initial idea of the logical structure.

More advanced features might be to try to use more of the text of the paper to assign some measure of importance to individual results (and then weight the diagram correspondingly to highlight the more important results), to try to give each result a natural language description, and to somehow capture key statements that are not neatly encapsulated in a theorem environment instance, but I would imagine that such tasks should be deferred until some cruder proof-of-concept prototype can be demonstrated.

Anyway, I would be interested to hear opinions about whether this idea (or some modification thereof) is (a) actually feasible with current technology (or better yet, already exists in some form), and (b) of interest to research mathematicians.

## 27 comments

Comments feed for this article

18 February, 2023 at 10:54 am

Máté WierdlHaving a tool that diagrams the structure of a paper could be a double edged sword. It’s possible that people would start writing papers in a way that would ease the work of the software, though that may not agree with what people find easy to understand. On the other hand, quite a few papers are written in a terribly non-structured way in which case it’s difficult to find proofs and logic, and the authors would benefit from structuring their documents better.

I think TeX/LaTeX is a good example how software can change papers’ presentations: it has become much easier to write formulas, copy them from one place to another in the paper, and as a result, authors often choose formulas over helpful explanations.

Personally, I like clearly structured papers (and slides), while I like books, from which I try to learn something, to be chatty, preferably with lots of pictures. Good luck with designing software that would try to draw a dependency diagram from an input file for these books, where well chosen words and pictures may carry the main content. :)

18 February, 2023 at 10:54 am

Keenan CraneHi Terry,

We’ve been working at CMU on a system called Penrose to “automatically” translate mathematics into diagrams: given purely logical statements (in plain text), generate and arrange visual icons that represent these statements. I put “automatically” in quotes since somebody has to say which icons are used to represent which statements. A bit more precisely, a collection of mathematical statements gets compiled into a constrained optimization problem; any solution to this problem is one possible diagram for the given statements. You can read about it here:

https://penrose.cs.cmu.edu/

https://penrose.cs.cmu.edu/siggraph20

And can try it out (in the browser—see gallery on left) here:

https://penrose.cs.cmu.edu/try

Best,

Keenan

18 February, 2023 at 11:23 am

Keenan CraneP.S. A bit more directly related to your post, the LEAN theorem prover community is integrating Penrose-generated diagrams into LEAN. Some discussion here: https://github.com/leanprover-community/mathlib4/pull/363

18 February, 2023 at 5:46 pm

AnonymousThat certainly sounds interesting and potentially useful, especially for long, complex papers. In the same spirit, would it be possible to have corresponding diagrams for the structure of long proofs? This may be in fact easier as a single proof is more self-contained and consistently organised than a whole paper, but it may also be hard as the steps and main arguments are not clearly labelled. I have made such diagrams for myself occasionally when reading a complex proof, it would be very helpful if they were available beforehand!

18 February, 2023 at 7:57 pm

AnonymousMicrosoft’s large language model based on GPT3.5+/4.0 from OpenAI could do this 0-shot with just a natural language prompt and LaTeX input, if you aren’t relying on the output diagram as a rigorous source of truth. A couple days ago I saw it successfully understand and respond to someone asking about algebraic geometry using LaTeX, and separately I saw it respond to someone else with a graphviz diagram of its understanding of its own behavior. Microsoft has since restricted its available functionality but maybe you can somehow get special access. If you have connections to access internal Google things, they probably have the capability as well.

14 March, 2023 at 10:32 am

gpt anonOriginal anon here but now I’m putting my email address in my post meta info. Today both the OpenAI/Microsoft GPT-4 and the Google PaLM APIs have been made available but by invitation only. Professor Tao, please feel free to let me know on email or below if you would like help using them to make the app; I don’t have access myself but I feel like you could get an invitation.

18 February, 2023 at 9:17 pm

arch1Possible wish list items for such a tool:

1) support optional author-provided tags (using syntax which fits as naturally as possible w/ typical paper flow) encoding info enabling better/more accurate diagrams

2) accept tool-generated diagrams, possibly human-tweaked, as part of the input. (e.g. for article revision n+1, the input diagram might be that for rev n; for article revision 1, it might instead be tagged as an exemplary diagram conveying subjective design choices)

18 February, 2023 at 9:24 pm

arch13) Make it ez to hide/delete some/all tags in final draft

19 February, 2023 at 10:55 am

NoviceGraphGPT makes knowledge graphs and if the proofs have some text clues scattered around the paper, perhaps what you ask can be done.

19 February, 2023 at 1:02 pm

AnonymousIt seems useful to indicate the new concepts, ideas and techniques in the paper.

19 February, 2023 at 4:14 pm

Automate your automation – The nth Root[…] As a result of the conference I started thinking about what possible computer tools might now be developed that could be of broad use to mathematicians, particularly those who do not have prior expertise with the finer aspects of writing code or installing software. One idea that came to mind was a potential tool to could take, say, an arXiv preprint as input, and return some sort of diagram detailing the logical flow of the main theorems and lemmas in the paper. … (Terry Tao) […]

20 February, 2023 at 7:53 am

BrunoThe goals here look very similar to the goals of the “Semantic Web”.

The proofs or papers don’t have to be written for automated theorem software,

they merely need to be attached with some metadata (which could be in the form of an tex comment or sidecar file).

The question is how one should encode the semantics of these entities.

A highly simplified example (a “classroom” scenario):

– have each proof bear a unique “identifier”

(could be randomly generated, like UUIDs and may bear auxiliary human readable names.

The identifiers themselves can be Uniform Resource Names (URN))

– 3 distinct proofs for “the same theorem” can be found in documents X, Y, Z.

(the documents are still subjected to the traditional review process)

– assign a unique identifier for “this theorem” (and a human readable name, possibly multiple names and multiple languages)

– link the identifiers of the 3 proofs above to the identifier of “this theorem”

(this will reside in some database which can get some sort of periodic publishes if

document form is desired)

IMO this whole process of tagging and linking identifiers is not completely unrelated to “citing” sources which

may ease the adoption for authors.

20 February, 2023 at 8:22 am

Lucas MorinMaybe instead of trying to predict a graph from a paper we can start by predicting a link from a sentence… Do you have enough labelled exemples ?

21 February, 2023 at 6:10 pm

Freddie MannersJust for my amusement, I tried getting ChatGPT to make something. Given the prompt:

“Can you write me some latex / tikz code for a flow diagram showing how the sections of a paper depend on each other? Specifically,

– There are 7 sections, 1-7.

– All the seconds depend on section 1.

– Section 4 depends on sections 2 and 3.

– Section 7 depends on sections 4,5,6.

– Sections 5,6 depend on section 4.

Also, the titles of these sections are:

– Section 1: introduction

– Section 2: preliminaries

– Section 3: a key lemma

– Section 4: the core argument

– Section 5: bootstrapping

– Section 6: a technicality

– Section 7: the proof of the main theorem.”

It produced:

“`

\documentclass{article}

\usepackage{tikz}

\usetikzlibrary{shapes.geometric, arrows}

\begin{document}

\begin{tikzpicture}[node distance=2cm]

% Define block styles

\tikzstyle{section} = [rectangle, rounded corners, minimum width=3cm, minimum height=1cm,text centered, draw=black]

\tikzstyle{arrow} = [thick,->,>=stealth]

% Nodes

\node (1) [section] {Introduction (1)};

\node (2) [section, below of=1] {Preliminaries (2)};

\node (3) [section, below of=2] {A Key Lemma (3)};

\node (4) [section, below of=3, xshift=-2cm] {The Core Argument (4)};

\node (5) [section, below of=4, xshift=-2cm] {Bootstrapping (5)};

\node (6) [section, below of=4, xshift=2cm] {A Technicality (6)};

\node (7) [section, below of=4, xshift=4cm] {Proof of the Main Theorem (7)};

% Arrows

\draw [arrow] (1) -‐ (2);

\draw [arrow] (1) -‐ (3);

\draw [arrow] (2) -‐ (4);

\draw [arrow] (3) -‐ (4);

\draw [arrow] (4) -‐ (5);

\draw [arrow] (4) -‐ (6);

\draw [arrow] (4) -‐ (7);

\draw [arrow] (5) -‐ (7);

\draw [arrow] (6) -‐ (7);

\end{tikzpicture}

\end{document}

“`

It does indeed compile. Some of the boxes overlap each other, but I guess it hasn’t figured that out yet. Otherwise I think it got everything right.

I think there is a real danger that by the time a dedicated tool had been completed, the next general purpose engine would be better than it.

[Apologies for any formatting weirdness.]

21 February, 2023 at 6:16 pm

Freddie MannersP.S. As shown, I always try to pose my questions to the engine politely. You never know — it might make all the difference some day.

23 February, 2023 at 12:31 pm

alonsoquixanoHi the latex document generated by ChatGPT does not compile for me (texlive2019) error is

./testproof-diagram.tex:22: Package tikz Error: Giving up on this path. Did you forget a semicolon?.

See the tikz package documentation for explanation.

Type H for immediate help.

…

l.22 \draw [arrow] (1) —

(2);

Uwe Brauer

23 February, 2023 at 8:47 pm

AnonymousIt looks like two consecutive hyphens were somehow changed into a long hyphen (m dash).

23 February, 2023 at 9:50 pm

Freddie MannersOh right, good catch — I tried to embed it as a code block but failed, and then WordPress outsmarted me and did all the usual formatting substitutions. Next time I’ll ask ChatGPT to output it in markdown directly.

[I think I managed to fix the hyphen formatting – T.]24 February, 2023 at 6:55 am

ObeyGPT (Beta)The same request yields this no-box-overlap code and makes me wonder if there is a fixed point theorem associated with repeated requests:

\documentclass{article}

\usepackage{tikz}

\begin{document}

\begin{tikzpicture}[->,>=stealth,shorten >=1pt,auto,node distance=3.5cm,

thick,main node/.style={rectangle,draw,font=\Large\bfseries}]

\node[main node] (1) {Introduction};

\node[main node] (2) [below left of=1] {Preliminaries};

\node[main node] (3) [below right of=1] {Key Lemma};

\node[main node] (4) [below of=2] {Core Argument};

\node[main node] (5) [below left of=4] {Bootstrapping};

\node[main node] (6) [below right of=4] {Technicality};

\node[main node] (7) [below of=4] {Proof of Main Theorem};

\path[every node/.style={font=\sffamily\small}]

(1) edge (2)

edge (3)

(2) edge (4)

(3) edge (4)

(4) edge (5)

edge (6)

edge (7)

(5) edge [bend right] (4)

(6) edge [bend left] (4)

(7) edge [bend right] (4);

\end{tikzpicture}

\end{document}

22 February, 2023 at 8:28 am

GianmarcoThis would definitely be(come) a great arXivlabs project.

(Maybe the technology behind ar5iv can also be used to this end?)

A similar tool has already been developed within LaTeX, using this package https://github.com/michal-h21/rdfref

See https://tex.stackexchange.com/questions/170480/show-graph-of-references-inside-a-document .

On a logical/design point of view, what about extracting “wiring diagrams” rather than graphs?

The string diagrams from the book “Seven Sketches in Compositionality” seem well suited for the task, allowing one to (black)box an argument, that can be used in another diagram.

But maybe this is for the future generations.

22 February, 2023 at 7:36 pm

AnonymousDiagramming tools have been around forever, “Pic” being an early example ( https://en.wikipedia.org/wiki/PIC_(markup_language) ). I think Graphviz ( https://en.wikipedia.org/wiki/Graphviz ) is a current favourite.

25 February, 2023 at 11:47 pm

ArmanPROF i shared this wounderful website in my Facebook page thanks for sharing YOUR experience with us)

26 February, 2023 at 1:54 am

ArmanPROF why i didn’t recive an email when YOU published new post thanks)

26 February, 2023 at 3:44 am

ArmanI wrote in my Facebook page that this is the best website to learn advanced mathematics)

9 March, 2023 at 11:46 pm

Yoann TrelluI manually created this graph, detailing the Pythagoras theorem using Tarski’s geometry and his book. The formatting is rather poor, nodes unlabelled, but the links are there.

Also very interested in tools for visualization, not only for math, but also for any process that can be modeled as a finite-state automata.. Applications to pedagogy & documentation would be significant!

10 March, 2023 at 5:39 am

Máté WierdlWhat does the pic mean? The dependence of chapters on the Pythagoras thm? And can you send a pic (or a link to it) with a much greater resolution? On this one, we cannot see what the nodes are.

10 March, 2023 at 6:15 am

Yoann TrelluCorrect, or to be more precise, the dependency on numbered lemmas, corollaries, propositions and theorems for the Pythagoras theorem (PT). It is a directed acyclic graph, whose source is PT, and sinks are Tarski’s axioms.

I’ll look into the associated graphviz code to see if I can link a better resolution image