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).
On November 30, 2020 4:34:17 PM PST, Igor Ieskov <[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/c779a1ce-76a4-4e9d-98bc-a6fd5085f4b1n%40googlegroups.com. -- 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/5D252348-45E2-479C-B3B9-A1422B720735%40panix.com.
