mm-site-format-userscript: Metamath proofs as calculations, with other readability improvements

[Marnix Klooster]

Hello all,

Here's a small thing I did to get used to one of those AI thingies, is build a successor to my earlier mm-calc2 browser userscript: https://github.com/marnix/mm-site-format-userscript.  (See the 'readme' document for installation instructions.)

As before, this makes your browser show a metamath.org theorem page's proof as a calculation; but this one also inserts whitespace and adds hover highlighting, all in the hope of more readability.

I still have some plans for updating this further, but it is already being quite useful for me.

Feedback e.g. via GitHub issues is welcome, enjoy!

Groetjes,

 <><

Marnix

[Marnix Klooster]

Hi all,

...and to show what this looks like, here is what a recently added theorem looks like, with that proof table replaced by a calculation version; and below that the improved proof table view, after switching back to the 'Table version' via the new link at the top right.

Let me know if this is useful to anyone.

Groetjes,

  <><

Marnix

The initial view of current nmulprop, with 0.11.0 of the mm-site-format userscript:

And then after clicking 'Table version' at the top right:

Op vrijdag 12 juni 2026 om 15:20:00 UTC+2 schreef Marnix Klooster:

[Marnix Klooster]

Hi all,

So in the past 3 weeks I've hacked some more on this userscript (version 0.28.0 has grown to ~3,000 lines of JavaScript code), and I must say that metamath.org proof reading is a lot more enjoyable for me now.  Also available via Greasy Fork now ( https://greasyfork.org/scripts/584794-mm-site-format ).

What do you think?

(I am wondering a bit why nobody is responding to this thread -- is installing a userscript a bottleneck? or doesn't anyone actually read the metamath.org proofs anyway? or would you want to see this in action before being tempted to try it out? or did you try it and it wasn't for you? or would you want this to be a separate 'normal' website? or did you try my earlier userscripts and you didn't like them?)

Feel free to let me know!

Groetjes,

 <><

Marnix

Op maandag 15 juni 2026 om 09:19:25 UTC+2 schreef Marnix Klooster:

[samiro.d...@rwth-aachen.de]

I just checked it out and think the foldable calculation view is a nice addition to the fixed table view.  (The "total installs" number didn't increase, so I suspect it is not working.)

> (I am wondering a bit why nobody is responding to this thread -- is installing a userscript a bottleneck? or doesn't anyone actually read the metamath.org proofs anyway? or would you want to see this in action before being tempted to try it out? or did you try it and it wasn't for you? or would you want this to be a separate 'normal' website? or did you try my earlier userscripts and you didn't like them?)

The only issue that comes to my mind with installing a userscript, apart from a few extra clicks to install a userscript extension, is probably checking that the script and extension can both be trusted. (I asked and pasted the script to Google AI and I am satisfied with the response.)

More generally, I am under the impression that in-depth interactions on this mailing list declined over the last 6 or so years. A lot of this is probably due to the absence of Norman Megill, who was an old-school thinker with a deep interest in his entire project. But I suspect that it is also due to people becoming more and more distracted and less interested in geeky stuff (and less intelligent; see reverse Flynn effect); especially since the web transformed into mostly a corporate-controlled place after it became mainstream. (So, basically the same reasons that most science forums died out.)

I wish we could present our today's contents to the web of the 90s and early 2000s; I am sure it would be much more fun and feel so much more alive. But in fact, we're drifting towards (and in many regards have already reached) a dystopian reality of general ignorance and corporate mind-control.

I am not one of the few people who are (still) enthusiastically engaged with Metamath Proof Explorer (MPE); I mostly use it to send links to people in order to make a point in discussions about related topics. But I would guess the enthusiasts are rather using their proof assistants to explore Metamath's database(s)?

Where I am really interacting with MPE's contents, I use my own software, which imports (propositional parts) of .mm files directly. I mentioned it a while back on this mailing list but didn't release it to the public since nobody was interested. (I converted some of its code to JavaScript to create an online syntax tree generator, though.) It displays proofs in (two) much nicer fashions and provides many additional features that I need.

[Steven Nguyen]

Some feedback on the whitespace, though note that I'm probably just used to the usual whitespace. The most common thing is the membership whitespace: nmulprop in the screenshot above still has an inconsistent spacing between A in On and x in On in the latest version. Similarly, my brain reads A. x in A as one idea, so the whitespace there isn't needed. Arguably this gets closer to "=" when the subexpressions are more complicated, so I understand it's complicated

Looking at a more complicated example, evlselv, perhaps a newline or 2x the whitespace could be considered for the highest level of many levels of whitespace, if there is sufficient amount of levels/complexity.

--
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 visit https://groups.google.com/d/msgid/metamath/535d2a27-f173-45b5-a939-edb44c452219n%40googlegroups.com.