Building the Mathematical Library of the Future

It is one thing to write it down in text, but something different to make it possible to interact with it. For me, this is a big step in the right direction.

What pops in my mind: This could be a very interesting base for further interaction layers such that it may be possible to not only proof, but derive intuitions via these interactions. These could be graphical visualizations, simulations, graphical playgrounds and so forth...

On the other hand there are already languages to proof theorems etc - I wonder what exactly the difference is (but I am no expert here, maybe if I would know these languages it is super obvious).

Hope this project gets the attention it deserves!