Metamath proof visualizer with graphs

[Matthias Vogt]

Hi everyone,

I wrote a cool visualizer for metamath proofs :3

 

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. 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 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 had LaTeX/Unicode support, that could be used for the visualizer for example.

Best

Matthias

[Mario Carneiro]

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...

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6fd3b538-ac91-431f-a476-9d79e4754b14n%40googlegroups.com.

[David A. Wheeler]

> On Jun 3, 2024, at 5:42 PM, Matthias Vogt <matthia...@gmail.com> wrote:
>
> Hi everyone,
> I wrote a cool visualizer for metamath proofs :3

You certainly did! It's really cool!

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. Here's an example:

[Thierry Arnoux]

That looks really cool indeed!

No problem to mirroring metamath.tirix.org of course.

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 ?

_
Thierry

[Johnathan Mercer]

Hi Mattias, 

Nice! did you use https://reactflow.dev/ ?

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStDO%2BphLRPGV63VGHzrc18vjej-72y2sfME8_QEMerCUw%40mail.gmail.com.

[Discher, Samiro]

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: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Johnathan Mercer <presc...@gmail.com>
Gesendet: Dienstag, 4. Juni 2024 01:46:42
An: meta...@googlegroups.com
Betreff: Re: [Metamath] Metamath proof visualizer with graphs

 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAHvyvqqG5_dH%2Bwr_1V0TPNjUryXyXVVMYSAifUHFRn-9QGNSxw%40mail.gmail.com.

[Matthias Vogt]

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?

[David A. Wheeler]

> On Jun 6, 2024, at 5:54 PM, Matthias Vogt <matthia...@gmail.com> wrote:
>
> 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?

Chrome on MacOS. However, I think what matters is that its setting "Appearance -> Font Size"
is set to "Very Large" (I have bad eyesight). Setting it to "Medium" makes the problem go away,
thought it should auto-adjust.

--- David A. Wheeler

[Discher, Samiro]

> 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: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Matthias Vogt <matthia...@gmail.com>
Gesendet: Donnerstag, 6. Juni 2024 23:54:11
An: Metamath

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f6027a4f-9fb9-4102-b31c-e560fb80de6en%40googlegroups.com.

[Matthias Vogt]

> I'd say make more space or make the containers scrollable for formulas that don't fit.

Thanks, it's fixed now -- not perfect but good enough.

> its setting "Appearance -> Font Size" is set to "Very Large"

Thanks, I fixed it and this works fine now