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.
