Hi Mattias, Nice! did you use https://reactflow.dev/ ?
On Mon, Jun 3, 2024 at 6:31 PM Mario Carneiro <[email protected]> wrote: > This is amazing and super awesome, and I will be using it in all my talks > from now on. :) It makes me more excited for getting that site rewrite > project moving forward... > > On Tue, Jun 4, 2024 at 12:27 AM Matthias Vogt <[email protected]> > wrote: > >> Hi everyone, >> I wrote a cool visualizer for metamath proofs :3 >> >> [image: Screenshot from 2024-06-03 20-54-43.png] >> It can... >> >> - Show the proof steps as an interactive graph >> - Show the proof as interactive nested proof blocks, from conclusion >> to premises >> - Summarize proofs and explain proof steps (I only hand-wrote >> explanation-functions for a few theorems, e.g. "by transitivity..." below) >> - Hide proof steps that you consider trivial, i.e. have a theorem >> number less than x >> >> You can view it (please use desktop) at https://vo.gt/mm/mpeuni/2p2e4 or >> add it as a tampermonkey extension <https://vo.gt/mm/extension.js>. You >> can replace "2p2e4" in the URL with any theorem you like. >> >> This is at the moment a super slow and hacky proof of concept and there >> are likely many bugs. The site above mirrors metamath.tirix.org (if it >> is not OK that I am mirroring math.tirix.org, please tell me and I will >> of course take down this demo site. It is not indexed by search engines or >> linked anywhere except here.). It also makes lots of requests to >> metamath.org to get the theorem numbers. Moreover, it runs the >> expln.github.io <https://expln.github.io/metamath/asrt/2p2e4.html> react >> code to get the substitutions that show us how theorems are used in proof >> steps. The code is basically an unmaintainable fever dream :p If there is >> interest, I might rewrite it in react at some point in the future. But I >> hope you like it anyway :) >> >> The basic idea for summarizing proofs is that smaller theorem numbers >> correspond to logic glue, so we can just not mention these theorems >> explicitly in the proof. Instead, when we have a non-trivial step, we just >> silently add the application of the trivial theorem to the resulting >> expression. The threshold for what is trivial customizable with the slider. >> Swallowing logic glue helps for readability, but still, in reality, I think >> what part of a proof is verbose is more of a stylistic decision by the >> author. >> >> What would make the visualizer even better is if there was a way to get >> LaTeX or Unicode output for the terms in the substitutions. But I don't >> know how to do this. If expln.github.io >> <https://expln.github.io/metamath/asrt/2p2e4.html> had LaTeX/Unicode >> support, that could be used for the visualizer for example. >> >> Best >> Matthias >> >> -- >> 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/6fd3b538-ac91-431f-a476-9d79e4754b14n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/6fd3b538-ac91-431f-a476-9d79e4754b14n%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/CAFXXJStDO%2BphLRPGV63VGHzrc18vjej-72y2sfME8_QEMerCUw%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJStDO%2BphLRPGV63VGHzrc18vjej-72y2sfME8_QEMerCUw%40mail.gmail.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/CAHvyvqqG5_dH%2Bwr_1V0TPNjUryXyXVVMYSAifUHFRn-9QGNSxw%40mail.gmail.com.
