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 On Monday, November 30, 2020 at 7:54:08 PM UTC-5 [email protected] wrote: > 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 > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/324292a1-0c90-4341-adf1-ed1d737bb7a7n%40googlegroups.com.
