On UIs to view Metamath database

[Ender Ting]

I'm thinking of some ways to make Metamath more accessible and more visually appealing.

Here's a concept art for axiom usage minimizers, for example.

(Blue colors are variants of Choice, red colors are either ax-3 or an axiom best avoided, others were randomly chosen.)

In single-theorem view, each proof step could have such a usage mask (we have 60 axioms not mechanically eliminable in set.mm right now, which fit into 5x12 grid neatly) and would allow to easily see the offending step.

Also among ideas is a better theorem search, which would not suggest steps unprovable from assertion's hypotheses, but it seems to require both SAT and some model of set theory. (A large language model might also fit; it must be remembering lots of math of various levels, to be thus able to generate counterexamples or proof guides.)

I'm yet checking how to parse the database, handle its parts and serve as a website; metamath-rs looks able to do that but it's documented a bit sparsely.

[Ender Ting]

I managed to build the text interface and convert it into HTML!

Next I'm going to emit HTML instead of text tokens, and also probably trim parentheticals from the right column. (Authorship is important, date of contribution is also nice to see, but the content of theorem is more important. These parentheticals could even be moved to the underfull left column.)

For example, now by absence of deep-blue axiom markers we see that Prof. Loof Lirpa hasn't yet had a choice in what to submit as his yearly research paper.

Contrast with:

I'd like to hear yours suggestions on what other information is worth it to infer from the database, as it may require me to choose another lib to parse it!

---

BW to every reader,

Ender Ting

пятница, 23 января 2026 г. в 07:44:12 UTC+3, Ender Ting:

[Ender Ting]

The view for browsing whole database is almost ready! Some code cleanup, and it might even be hosted.

(I also aim to have update time faster than a day for the merged changes.)

понедельник, 26 января 2026 г. в 06:01:48 UTC+3, Ender Ting: