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]<mailto:[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]<mailto:[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]<mailto:[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]<mailto:[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]<mailto:[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/bc1cdba2626540ad8582917ddcec4d74%40rwth-aachen.de.
