Thanks everyone for the compliments c: > I did find a minor problem with the graph display - the bottom part of the text > labels gets cut off. E.g., in "eqtr4i" you can't tell it's a "q" because the bottom > tail is cut off. I suspect a minor tweak would fix it. I can't reproduce this in chrome or Firefox unfortunately, what browser are you using?
> For printing LaTeX or Unicode for the terms in the substitutions, maybe there could be some web service serving the HTML version, whenever provided with ASCII ? That would work, or if https://expln.github.io had support for this, that would also work > Nice! did you use https://reactflow.dev/ ? Thanks for the recommendation, It's just vanilla javascript and d3.js but for a rewrite I would use react. > the visualizer looks somewhat hilarious / messy for proofs with large formulas: https://vo.gt/mm/mpeuni/retbwax1#triv1733 Fixed, thx Do you have any suggestions for improvement or feature ideas? [email protected] schrieb am Donnerstag, 6. Juni 2024 um 01:52:18 UTC+2: > This looks really damn cool. > Though the visualizer looks somewhat hilarious / messy for proofs with > large formulas: https://vo.gt/mm/mpeuni/retbwax1#triv1733 > ------------------------------ > *Von:* [email protected] <[email protected]> im Auftrag von > Johnathan Mercer <[email protected]> > *Gesendet:* Dienstag, 4. Juni 2024 01:46:42 > *An:* [email protected] > *Betreff:* Re: [Metamath] Metamath proof visualizer with graphs > > 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 > > <https://groups.google.com/d/msgid/metamath/CAHvyvqqG5_dH%2Bwr_1V0TPNjUryXyXVVMYSAifUHFRn-9QGNSxw%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/f6027a4f-9fb9-4102-b31c-e560fb80de6en%40googlegroups.com.
