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: