Visualization of theorem relationships A few minutes ago a thought for a website/program crossed my mind and now I somehow hope that such a thing already exists. I thought of:


*

*A set of theorems linked by arrows telling the viewer/reader eg. that (the "typical" proof) of Theorem A is based on Theorem B which is just a corollary of Theorem C etc.

*At least in my head a 2D or even 3D visual representation which "more complicated" theorems at the top and theorems arranged by field (or with minimal arrow distance, which could be nearly the same) makes a cool visualization.

*Different fields could even be differently colored.

*I guess some very basic and/or fundamental theorems have to be excluded in order to do not mess up the graph.

*Similarly one cannot include the ~$10^\text{large number}$ many fields of mathematics (or at least you need "turn field foo on/off" buttons") – but maybe you can include theorems normally proven in the first university years or something like that? (I would even appreciate a graph of a single field, complex analysis for example could look really cool on its own.)

*Bonus points, if clicking on the graph (or even the arrows!) yields information about the theorem (or the proof).

*Of course this has to be somewhat biased. Example: Is Picard Lindelöf "typically proven" by the Banach Fixpoint Theorem? Or should the graph rather include similar fixpoint theorems which are still sufficient to prove Picard Lindelöf? Lots of bonus points for a nice way to circumvent such problems.

*Another problem might be something like "A is proven very hard by … and then B, C and D follow easily. Alternatively, one could have proven D in a totally different way then A and then work "backwards" to A. Bonus points again, if this is visualized nicely.

*There are probably lots of more points I could add here, most of them containing the "bonus points for" phrase, but I will stop here.


My question is:


*

*Is such a graph possible to create?

*Are there any problems with this idea (apart from doing lots of work just for a nicely looking graph of course)? For example would it just look awful and no one could see anything between thousands of arrows?

*Even better, is there already an existing project?

 A: Given the following definition and theorems:


*

*Let $\sum_{n=1}^{+\infty} u_n$ be a given infinite series, and let $\{s_n\}$ be the sequence of partial sums defining this infinite series. Then if $\lim_{n \to \infty} s_n$ exists and is equal to $S$, the given series is convergent. If $\lim_{n \to \infty} s_n$ does not exist, it is divergent.

*If the infinite series $\sum_{n=1}^{+\infty} u_n$ is convergent, then $\lim_{n \to +\infty} u_n = 0$.

*If $\lim_{n \to +\infty} u_n \ne 0$, then $\sum_{n=1}^{+\infty} u_n$ is divergent.


The relationships between the definition and theorems are simple to graph:

But, given this additional theorem:


*

*Let $\{s_n\}$ be the sequence of partial sums for a given convergent series $\sum_{n=1}^{+\infty} u_n$. Then for any $\epsilon > 0$, there exists a number $N$ such that $|S_R - S_T| < \epsilon$ whenever $R > N$ and $T > N$.


The relationships between this theorem and the others suddenly becomes much more complicated to graph. If the visualization is more complicated than the theorems, then that might indeed be a problem.
