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.
