Visualization of proofs with javascript and SVG

[Igor Ieskov]

Hi all,

I want to share with you an example of how proof steps could be visualized to improve readability. When I was trying to understand how Metamath works, I wrote a java program which does verification of theorems according to the Metamath book (just to ensure that my understanding is correct). After that I made an addition to that program to visualize content of the stack with proof steps. Basically this program converts set.mm file to a set of html files with proofs visualizations. I found such visualization very useful for me and I want to share it with you.

Please find attached a screenshot of one of such proof visualizations.

I temporarily placed those generated html files on a web server (though I am not sure how long it will stay online) http://metamath.d4-e5.de/index.html  Those html pages contain json data and javascript code which visualizes the data using SVG. It is not optimized, so for some big proofs it may slow your browser down significantly.

Here are few direct links to proofs in case if index.html doesn’t work for any reason:

http://metamath.d4-e5.de/data/2p/2e/2p2e4.html

http://metamath.d4-e5.de/data/sq/rt/2i/sqrt2irr.html

I tested this in Chrome and Firefox only, but I hope it works in other browsers too.

Also there is a link to zip archives with those generated html files:

https://drive.google.com/drive/folders/1na2UM270rsCd85BQCmaJJSnak8HywfL8?usp=sharing

• all-assertions--metamath-proof-explorer.zip - contains all axioms and theorems from set.mm and when unarchived it takes 900M.

• first-193-assertions--proof-explorer.zip - takes only 2M when unarchived.

And here is the repo with the program https://github.com/Igorocky/text-parser (I am sorry for the “cleanliness” of the code, it is a proof of concept and I am not sure it will be interesting to anyone else except of me).

I am not a mathematician and I am a novice to Metamath, so I am sorry if this is useless or too primitive. I just found it very helpful for me to understand proofs and I think it may be helpful for others who are also novice to proof formalization.

Best regards,

Igor Yeskov

[Norman Megill]

I like this.  I think that showing explicit substitutions like this could be very helpful to a beginner trying to learn how to follow Metamath proofs.

Lest it be forgotten, another experiment that shows explicit substitutions is here::

http://us.metamath.org/mpeuni/_mmbrows2p2e4.png

This was done by Paul Chapman around 2007 I think.  AFAIK this was just a proof of concept experiment, and he didn't publish the program that generated it.

Norm

[Jim Kingdon]

Oooh nice. I would have found this quite useful when I was learning about all the "glue" theorems which many proofs use like syl, syl2anc, adantr, etc. Might still find something like it useful (especially if there were a way to click something to show it for a particular step, or something else more selective than having it always be present).

[Paul Chapman]

Norm wrote:

 

> Lest it be forgotten, another experiment that shows explicit substitutions is here::

> http://us.metamath.org/mpeuni/_mmbrows2p2e4.png

> This was done by Paul Chapman around 2007 I think.

> AFAIK this was just a proof of concept experiment, and he didn't publish the program that generated it.

 

So long ago. The program was written for Smalltalk/V Win, and I’ve never been able to get this Smalltalk  running under Windows 7. And the AMD chip that came with this computer won’t run XP under VirtualBox (this is a known problem, and was bad luck).

 

Planning for my next PC to be Windows 10 on an Intel with virtualization. So you never know.

 

I may be getting too old/lazy to code. Thirty years ago I’d’ve written a knockout replacement for mmj2. ;)

 

Back to lurking.

 

Cheers, Paul

[Jim Kingdon]

On 11/30/20 6:03 PM, Paul Chapman wrote:

> I may be getting too old/lazy to code. Thirty years ago I’d’ve written
> a knockout replacement for mmj2. ;)

Haha I'll let you be the judge of whether you are too old/lazy to code.

But if you are just disinclined to shave all the yaks required to get a
smalltalk compatible with that experiment running again, hey that
strikes me as quite understandable quite aside from age. Quite a saga.

[Igor Ieskov]

Norm, Jim, thanks for your feedback!

I updated the proof visualisation - all steps are collapsed by default and a [+] button will expand selected node. Examples:

http://metamath.d4-e5.de/v2/data/2p/2e/2p2e4.html

http://metamath.d4-e5.de/v2/data/sq/rt/2i/sqrt2irr.html

http://metamath.d4-e5.de/index.html

Also offline version may be found here https://drive.google.com/drive/folders/1na2UM270rsCd85BQCmaJJSnak8HywfL8?usp=sharing (its size is 500M when unarchived).

At the moment, step numbers in my proof visualisation don't correspond to step numbers on http://us.metamath.org in many cases. This is because of duplicate steps in my visualisation. I will fix this.

Best regards,

Igor

вторник, 1 декабря 2020 г. в 03:22:00 UTC+1, kin...@panix.com:

[Norman Megill]

When this becomes stable, I can add a link to your version on each theorem page of the main site, like the link that now says "Structured version" for Thierry's pages.  This will let you have direct control over your content.  (To start with, your base URL would be hard-coded in metamath.exe, but later I can add a keyword to the $t statement in set.mm so the URL can be maintained there.)

I don't know your long term plans, but I'll mention that personally (although I may be in the minority) I don't mind the ASCII notation in the proofs.  It shows a beginner the direct relationship to the set.mm source and allows easy copy/paste.  The user can also see the direct relationship between the ASCII and the Unicode rendering by switching between your page and the standard page, without having to consult set.mm or the awkward "ASCII Symbol Equivalents" page.

BTW although of course it's not as convenient as your pages, some people might not know that metamath.exe can show the substitutions made in a step:

MM> show proof 2p2e4 /detailed_step 18

Proof step 18:  eqtr4i.1=oveq2i $p |- ( 2 + 2 ) = ( 2 + ( 1 + 1 ) )

This step assigns source "oveq2i" ($p) to target "eqtr4i.1" ($e).  The source

assertion requires the hypotheses "cA" ($f, step 13), "cB" ($f, step 14), "cC"

($f, step 15), "cF" ($f, step 16), and "oveq1i.1" ($e, step 17).  The parent

assertion of the target hypothesis is "eqtr4i" ($p, step 47).

The source assertion before substitution was:

    oveq2i $p |- ( C F A ) = ( C F B )

The following substitutions were made to the source assertion:

    Variable  Substituted with

     C         2

     F         +

     A         2

     B         ( 1 + 1 )

The target hypothesis before substitution was:

    eqtr4i.1 $e |- A = B

The following substitutions were made to the target hypothesis:

    Variable  Substituted with

     A         ( 2 + 2 )

     B         ( 2 + ( 1 + 1 ) )

Norm

[Igor Ieskov]

Yeah, that would be an honour for me to make a contribution to Metamath. Sure, I want to solve few technical issues, test them during some time and then you can add links.

I also thought regarding unicode symbols. I will spend some time to try to add possibility to show both ascii and unicode symbols (but I don't promise to do it fast enough because of lack of time :) )

Actually I've just figured out that I can use this feature of metamath.exe to verify what my program generates. This is not straightforward though but possible. 

I will write a message when I think this my visualisation is stable enough so we can start adding links.

Best regards,

Igor

вторник, 8 декабря 2020 г. в 17:13:15 UTC+1, Norman Megill:

[Igor Ieskov]

Hello Norm,

I’ve prepared a final version of my proof visualizations which you may add links to on the main site. URLs of pages have a form of https://expln.github.io/metamath/asrt/label.html  Where “label” should be replaced with the actual label of an assertion. (“asrt” stands for “assertion” and it is a constant part of the URL) For example: https://expln.github.io/metamath/asrt/sqrt2irr.html

I spent some time investigating if I can implement unicode representation but it appeared complicated because each symbol is represented as raw html code. And it is not trivial to embed it into SVG visualization.

Please let me know if everything is ok and you can add links to this version.

Best regards,
Igor

вторник, 8 декабря 2020 г. в 20:17:37 UTC+1, Igor Ieskov:

[Benoit]

That looks great. Congratulations!

Benoît

[Norman Megill]

I like this very much.  I think I will add a variable to the $t statement in set.mm so your base URL can be maintained there, instead of being hard-coded in metamath.exe.  (And Thierry's structured version also, which is currently hard-coded.) Give me a week or so.

An observation (in Chrome 87.0.4280.88 at least):  when the [+] box is clicked, the [-] box sometimes appears in the lower-left corner of the expanded table cell and other times in the upper-left corner.  E.g. step 34 of sqrtirr shows a lower-left [-]  and step 35 shows an upper-right [-].  Ideally the [-] would remain at the same position as the corresponding [+] so we can open and close an expansion without moving the mouse, although I'm not sure how hard that is to do.

Norm

[Norman Megill]

On Sunday, December 20, 2020 at 11:13:33 AM UTC-5 Norman Megill wrote:

I like this very much.  I think I will add a variable to the $t statement in set.mm so your base URL can be maintained there, instead of being hard-coded in metamath.exe.  (And Thierry's structured version also, which is currently hard-coded.) Give me a week or so.

An observation (in Chrome 87.0.4280.88 at least):  when the [+] box is clicked, the [-] box sometimes appears in the lower-left corner of the expanded table cell and other times in the upper-left corner.  E.g. step 34 of sqrtirr shows a lower-left [-]  and step 35 shows an upper-right [-].  Ideally the [-] would remain at the same position as the corresponding [+] so we can open and close an expansion

s.b. "upper-left"

[Igor Ieskov]

Thanks Benoit and Norm!

I will try to fix this behaviour of +/- button. (it happens in all browsers)

Best regards,

Igor

воскресенье, 20 декабря 2020 г. в 17:35:35 UTC+1, Norman Megill:

[Igor Ieskov]

The problem with the “jumping” [-] button is fixed. I also added few more features:

1) Adjustment of column widths: click a “three horizontal lines” button at the top right corner of the proof table. Column widths are stored in the local storage of the browser, so width adjustment may be done only once and it will be applied to all other assertion pages unless local storage is turned off.

2) Highlighting of matching parentheses: hover the mouse over a parenthesis to temporarily highlight it or click it to highlight it permanently. This feature works only on unexpanded expressions. 

Best regards,

Igor

воскресенье, 20 декабря 2020 г. в 17:46:28 UTC+1, Igor Ieskov:

[Norman Megill]

This is great!

A slight cosmetic issue is that the Ref column sometimes overflows into the Expression column for long theorem names, e.g. https://expln.github.io/metamath/asrt/merco1lem18.html
Ideally the Ref column width should automatically be resized to the longest theorem name.

I modified metamath.exe to recognize a new $t keyword "htmlexturl" (HTML external URL) that is now in set.mm on GitHub. Your visualization version is linked to on each theorem page now (on the us2 server) e.g.

http://us2.metamath.org/mpeuni/sqrt2irr.html

NOTE TO EVERYONE: metamath.exe was updated on GitHub to "Version 0.194 26-Dec-2020" to recognize the new $t keyword. You will need to update it locally for "verify markup" to pass with the set.mm change I made, either from GitHub or http://us2.metamath.org/index.html#mmprog . If you are using Windows, the 0.194 executable can be retrieved here:
http://us2.metamath.org/metamath/metamath.exe

Norm

[Igor Ieskov]

Thanks Norm. I updated my visualization, so column width is calculated automatically now.

Best regards,
Igor

воскресенье, 27 декабря 2020 г. в 18:17:56 UTC+1, Norman Megill: