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
On 03/06/2024 23:42, Matthias Vogt 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
(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/05396329-9b7d-4d61-96df-3669e20c03f7%40gmx.net.
