Metamath visualization

[void4]

http://de.metamath.org/index.html http://paperscape.org/ https://d3js.org/

Excerpt from a conversation with Norman Megill:

1. Would an interactive visualization, possibly similar to http://paperscape.org/ make sense?

Off and on I've tried to imagine what such a display would look like (in 2D or even in 3D like those 3D fractal navigation videos on Youtube) but haven't come up with any good ideas. One problem is that each proof may depend on thousands of earlier theorems in a gigantic tree, and I don't know how to represent something like that in a meaningful way. Not to mention that I have little expertise at graphics work.

But there are a lot of people more clever than me, so someday someone may come up with a visually appealing method.

2. Is there any interest in the creation of a web based proof editor?

Probably not a strong interest, since we already have the well-developed mmj2 GUI proof editor that most people use. Collaboration is usually done via GitHub with pull requests that we want to approve in order to maintain a high quality database (set.mm). This seems to work well. So right now I don't foresee a time when the database will be edited directly on-line, but that may change.

One attempt at an on-line editor for Metamath was http://mm.ivank.net/ but it doesn't seem to be worked on right now or used much. (I'm not very familiar with its capabilities.) The page http://us.metamath.org/other.html has a list of various other projects people have worked on for Metamath.

The project Wikiproofs http://wikiproofs.org/ allows directly entry of proofs to its database, but it hasn't been as popular as Metamath for some reason and has a very long way to go before it has a proof library the size of Metamath's. Its language is based on Ghilbert, which has been evolving slowly as a kind of spin-off of Metamath.

3. Would it be possible to use or extend the formal language to allow for the integration of physical assumptions and observations in order to reason about them?

In principle, yes, since they are just mathematical statements with assumptions. I would like to see some of that as a long-term goal, especially since mathematical rigor is often lacking in many physics textbooks. The Hilbert space work in set.mm explores some aspects of the mathematics for quantum mechanics.