Hey all, I accidentally ran into metamath and immediately fell in love with the concept. I started building a parser, a verifier and some visualizations to help me understand how and why it worked.
It is not much different from what has already been posted before (except, maybe, that's all done client-side on the web), but I figure you'd all appreciate an independent parser, verifier and visualizer out there. So, here it goes: Source Code https://github.com/samuelgoto/metamath Set.mm's client-side verification (takes ~1 min in my macbook m1) https://code.sgo.to/2022/11/26/set.mm.html 2p2e4 Visualization (takes a while to load, but once it does, you can navigate easily) https://code.sgo.to/2022/11/26/2p2e4.html Hoffstader's systems: https://code.sgo.to/2022/04/17/hofstadter-tq.html https://code.sgo.to/2022/04/13/hofstadter-pq.html https://code.sgo.to/2022/04/12/hofstadter-miu.html If you dig into my blog, you'll likely find why I ran into metamath and why I find it so interesting: https://code.sgo.to/ Good stuff you all, Hope this helps, Sam -- 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/23d122fd-021d-4e59-9281-b485d687c047n%40googlegroups.com.
