> Do you have any suggestions for improvement or feature ideas?
Apparently, you have already fixed the overlays by just cutting formulas off. I'd say make more space or make the containers scrollable for formulas that don't fit. ________________________________ Von: [email protected] <[email protected]> im Auftrag von Matthias Vogt <[email protected]> Gesendet: Donnerstag, 6. Juni 2024 23:54:11 An: Metamath Betreff: Re: [Metamath] Metamath proof visualizer with graphs 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 [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<http://metamath.tirix.org> (if it is not OK that I am mirroring math.tirix.org<http://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<http://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]<mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f6027a4f-9fb9-4102-b31c-e560fb80de6en%40googlegroups.com<https://groups.google.com/d/msgid/metamath/f6027a4f-9fb9-4102-b31c-e560fb80de6en%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/0ec73112446f47579bc05ee2c7b8cee5%40rwth-aachen.de.
