Yes, very impressive! And yes, I believe the client-side proof explorer
does break new ground - I was edging in that direction, but quite slowly.
Is the (React) source code for that around anywhere? I see you're trying
to get it all streaming, presumably so you can parse and display proofs as
soon as that part of the file is downloaded without having to wait for the
whole thing to arrive (a download progress bar would be great too). All
things I was planning to do eventually.
Nice to see standard lexer and parsing tools in your verifier too. Would
you consider adding a licence to the package.json file? It looks very
reusable!
Best regards,
Antony
On Tue, Nov 29, 2022 at 9:47 AM Samuel Goto <[email protected]> wrote:
> 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
> <https://groups.google.com/d/msgid/metamath/23d122fd-021d-4e59-9281-b485d687c047n%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAJ48g%2BBkK%2B2p%3D4K4wdwdZXZWx8kOqKMgz%3DHz9FderKFxCmKfpQ%40mail.gmail.com.
