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.
45 comments
Comments feed for this article
18 February, 2023 at 10:54 am
Máté Wierdl
Having 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 Crane
Hi 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 Crane
P.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
Anonymous
That 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
Anonymous
Microsoft’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 anon
Original 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
arch1
Possible 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
arch1
3) Make it ez to hide/delete some/all tags in final draft
19 February, 2023 at 10:55 am
Novice
GraphGPT 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
Anonymous
It 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
Bruno
The 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 Morin
Maybe 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 Manners
Just 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 Manners
P.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
alonsoquixano
Hi 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
Anonymous
It looks like two consecutive hyphens were somehow changed into a long hyphen (m dash).
23 February, 2023 at 9:50 pm
Freddie Manners
Oh 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
Gianmarco
This 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
Anonymous
Diagramming 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
Arman
PROF i shared this wounderful website in my Facebook page thanks for sharing YOUR experience with us)
26 February, 2023 at 1:54 am
Arman
PROF why i didn’t recive an email when YOU published new post thanks)
26 February, 2023 at 3:44 am
Arman
I wrote in my Facebook page that this is the best website to learn advanced mathematics)
9 March, 2023 at 11:46 pm
Yoann Trellu
I 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é Wierdl
What 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 Trellu
Correct, 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
22 March, 2023 at 5:17 pm
liuyao
It’s very nice to see all the different attempts, as that’s something I’ve thought to do. Here’s what I left off, if it’s of any use, https://observablehq.com/@neobourbaki/tools . Basically it relies on digraph, a javascript tool, to draw directed graphs with simple commands (you specific the nodes and arrows, and they arrange everything in a plane). Not so much easier than tikz, but one could try to take a LaTeX file as input…
22 March, 2023 at 9:26 pm
Marcelo
What (if anything) is the “Scrivener for math papers”? It wouldn’t help with what was already written, but improving structure-inducing writing tools might be an easier technical ask than structure-inferring reading tools. (I’m thinking of the “semantic” aspects of Scrivener, not just facilities for links or outlining.)
24 March, 2023 at 8:15 am
chevallier augustin
I have been working on some software to solve this exact question:
https://github.com/augustin-chevallier/MathResultsGraph
It takes a Latex file (where the dependency between theorems/ lemmas are manually added), and then creates an interactive graph that can be displayed/edited in a webpage.
Here is some WIP example: http://www.emmanuelchevallier.eu/graphSite/graph_split.html
24 March, 2023 at 8:17 am
chevallier augustin
Here is an example screenshot (which I hope will be displayed by wordpres…):
26 March, 2023 at 3:56 am
J
ChatGPT can definitely do it
29 March, 2023 at 4:35 am
Terence Tao
Uwe Brauer pointed me to some latex style files at https://github.com/michal-h21/rdfref that allow for generation of dependency graphs provided that some relevant metadata tags are added to the relevant theorems one wants to link.
I have tried briefly to use GPT-4 to create these graphs (or at least to summarize a paper in terms of such dependencies) but ran into the problem that the size of a typical math paper is longer than the allowable prompt size. It is capable though of summarizing the key points of a paper based on its introduction, which is sort of similar to what I had in mind.
29 March, 2023 at 5:35 am
alonsoquixano
I have tried out rdfref successfully but failed, for the moment, with MathResultsGraph, basically because the latter relies on python and my Ubuntu version seems to ship a version that is not recent enough. I also struggled to use it with MacOs, but I might solve this issue. Be it as it may, both approaches require the author to add some metadata (and to provide some style files), so I am skeptical that this could be done for arXiv manuscripts in an automated way, as Terence Tao asked. I also thought that the goal was to generate a kind of visual (logical) dependence of theorem, lemmas etc, so I am curious to see what GPT-4 was able to produce.
Uwe Brauer
29 March, 2023 at 7:16 am
alex
There are two sub-versions of GPT-4: one with an 8K tokens context window and one with 32K tokens. Maybe you could specifically ask for access to the 32K version if you don’t have it already?
4 April, 2023 at 5:10 am
Terence Tao
I’ll look into this, though it may well be that the simplest option is to wait a year until something like GPT4.5 with an internet plugin comes out, at which point it may be able to achieve the goal of my blog post (and much more besides) through a simple prompt or API call.
In the meantime, I have come across the experimental project “Ask Paper” (still in beta) which can take a paper (or URL to such a paper, e.g., an arXiv link) as input and then answer questions about it, ChatGPT-style. The AI does not seem to be quite as advanced as GPT4 and could not simply produce a diagram, but was able for instance to identify the important propositions and theorems in the paper, and say something about their logical relationship. It’s possible that one could combine this tool with one of the diagramming software solutions mentioned elsewhere in comments (together perhaps with some use of a GPT4-level LLM to translate the output of the former tool into a format suitable for the latter tool) to achieve some rudimentary version of the one-click diagramming tool that I had in mind, but it may be a bit clunky at the current level of technological development.
4 April, 2023 at 7:43 am
alonsoquixano
Thanks for the link: I just tried it out. Fun fact: If you register, the interface is confusing, if you stay as a guest, the interface is rather straightforward.
I choose an arXiv preprint and selected the option: summary, but I was not convinced by the result: the software just gave a short summary of each section, without mentioning the important theorems, lemmas and the logical structure between theses. Maybe one needs to refine the task.
17 April, 2023 at 7:36 am
Terence Tao
I have recently come across another project, “ChatPDF“, which has a simple interface and does seem to be intelligent enough to isolate the key results of a paper and their logical dependencies, so this (combined with some diagramming tool) may already be a sufficient solution to the original problem.
17 April, 2023 at 12:13 pm
alonsoquixano
Hi thanks for ChatPDF, I tried it out with one preprint I had at hand. I asked the system which lemmas are used to prove the main result, and he talks about lemma 2.9 and 2.10, alas both do not exist. There is proposition 2.10 but this is not relevant for the proof. So I am not sure what is going on…. It is a free tool, but…
19 April, 2023 at 12:47 pm
Terence Tao
Hmm, it does seem that the tool is not always reliable (though I have found that if you follow up by giving it more guidance, for instance by providing examples of what you are looking for, it can correct itself after its initial response – somewhat like guiding a confused undergraduate during office hours). It seems this tool relies on GPT3.5 which does have a limited number of tokens it can process at a time; perhaps a future version of the tool would use something like GPT4 which can process many more tokens and I would expect it to be significantly more accurate (this may require a paid subscription though).
20 April, 2023 at 11:56 am
alonsoquixano
> Hmm, it does seem that the tool is not always reliable
Maybe I was not patient enough. I will give it another try with a paper I know well and try out a series of questions, as you indicate. In any case, this tool seems unable to generate a visual map of the structure of the paper, as you described in your first post. (maybe in the coming years)
20 April, 2023 at 9:30 am
Anonymous
ChatGPT only tries to continue the conversation, it doesn’t understand what it says, or anything else that resembles a human. How humiliating to compare it to an undergraduate student? or any human for that matter.
16 April, 2023 at 2:44 am
xiha
https://paperswithcode.com/dataset/ai2d here is a dataset GPT4 has 78.2% on this dataset with 0-shot
16 April, 2023 at 2:47 am
xiha
The dataset is called AI2D (AI2 Diagrams)
25 April, 2023 at 9:17 am
Andrew Krause
Somewhat orthogonal to this, but in a similar spirit: We’ve recently released a new website, VisualPDE.com, for real-time and interactive solutions of partial differential equations. Really I’d encourage you to click through and play with some examples (or type in your own PDE and solve it in 1D or 2D etc). It works on most phones or computers, and uses the native web browser (and the devices’ GPU) to perform the numerical simulations in real time.
More generally very keen to see more interactive mathematics be developed. I think these ideas are all potentially quite transformative…