Metamath website

106 views
Skip to first unread message

Thierry Arnoux

unread,
Jan 11, 2022, 10:48:37 PM1/11/22
to metamath

Hi all,

Norm was manually updating the Metamath web pages and so they still stand at their state of beginning of December. Some have expressed their wish to see updated pages.

I've written a short web server for Metamath web pages, metamath-web, and I'm now running it on http://metamath.tirix.org:3030/mpests/tgoldbachgt.html.

It serves the pages dynamically, meaning that it has parsed set.mm, and then builds and serves the pages on the go as they are requested (I can't help mentioning here Mario described that as super-cool in a recent comment ;) ).

For now, it only serves set.mm pages. It would not be very hard to extend it to e.g. iset.mm.

There are only two renderers implemented until now:

  • the unformatted ASCII source file, which uses "mpeascii" in the path,
  • the so-called "structured typesetting" (STS), with "mpests" in the path.  

I've not yet implemented a unicode renderer (as in "mpeuni") but this shall be pretty straightforward once parsing the $t typesetting section of metamath files is implemented.

This is still very much experimental and incomplete, so of course it does not compare with all the functionalities built in over the years in the metamath-exe pages, but I wanted to already share it. Here are some features which are still lacking, roughly in the order I'd like to add them:

  • only theorems are displayed, axioms and definitions are not (pages are in error). I will put there the "syntax proof" as in the original web pages,
  • theorems hypotheses and final statement are not shown at the top of the page, it's just the proof right now, so the final statement is at the very bottom of the page,
  • there is no navigation to the next/previous theorems in the database,
  • there is no table of content,
  • the embedded math in-line in comments between `` is not formatted,
  • the $d distinct variables are not displayed,
  • the "used by" list is not built.

To update the pages, I have to manually fetch the new set.mm version and restart the server. This however is very lightweight and takes only a few seconds, compared to the regeneration of a whole directory with 30000+ files. I believe this can be automated.

The server code is roughly 300 lines of code, plus another 200 for STS, so it shall not be too hard for anyone to join its development - any help is welcome!

I hope this utility will help others discover some the latest theorems which are not yet on the us2 server:

Sorry for those I missed! There is of course Jim's intuitionistic proof of Bezout's theorem, I hope I can setup the server soon for iset.mm!

BR,
_
Thierry


David A. Wheeler

unread,
Jan 12, 2022, 11:32:49 AM1/12/22
to Metamath Mailing List
Thierry, thanks so much!! I still intend to re-update the Metamath website, but other life events have been all-consuming.
I'm hoping to get to it this weekend :-(.

--- David A. Wheeler
> --
> 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/8899df6a-4d70-d72a-585f-1131f7857075%40gmx.net.

Scott Fenton

unread,
Jan 12, 2022, 12:28:55 PM1/12/22
to meta...@googlegroups.com
That's awesome! I'd love to help and I've got some time off coming up. Where can I grab the source code to give it a whirl?

> On Jan 12, 2022, at 11:32 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
> Thierry, thanks so much!! I still intend to re-update the Metamath website, but other life events have been all-consuming.
> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9E07EBC1-1545-4E5B-8C86-475EE5053876%40dwheeler.com.

Thierry Arnoux

unread,
Jan 12, 2022, 12:44:39 PM1/12/22
to meta...@googlegroups.com, Scott Fenton
Hi Scott!

That would be awesome!

The source code is on GitHub here: https://github.com/tirix/metamath-web

_
Thierry

Glauco

unread,
Jan 12, 2022, 1:40:55 PM1/12/22
to Metamath
Great job, Thierry.

Benoit

unread,
Jan 12, 2022, 2:44:09 PM1/12/22
to Metamath
Thanks Thierry, this looks great !

Both "ascii" and "mathml/mathjax" are useful (the latter may lure more people to metamath), and I hope "unicode" will be available soon.  Actually, for metamath.org, I have been thinking for some time that gif support could be deprecated and replaced with "ascii".

Where you mention the navigation links next/previous, it would also be nice to have links to toggle between the three versions (ascii, unicode, mathml/mathjax) of the currently displayed theorem (and maybe also a link to the corresponding metamath.org page).

Concerning your ~tgoldbachgt : it looks like the conclusion should be Step 127: no need to go to the more complicated Step 135, which does not bring anything. (?)

Benoît

Thierry Arnoux

unread,
Jan 12, 2022, 9:01:14 PM1/12/22
to meta...@googlegroups.com, Benoit

Hi Benoît,

Yes, links between the different typesetting would be useful and shall be something quite easy to add!

You're very right about ~tgoldbachgt . That intermediate state is better and just as strong. I made the few last extra steps because I wanted to state that theorem exactly the way ~ ax-tgoldbachgt is written in your mathbox.

There is even a compact version without any bounded variable: ` ( ( ZZ>= ` ( 10 ^ 27 ) ) i^i Odd ) C_ GoldbachOdd `

I can change that statement and provide both those versions. What would really be great is if you could use that theorem (or one of the newer versions of it) in your mathbox in place of ~ ax-tgoldbachgt to "close the loop" and make the link between both developments!

BR,
_
Thierry
--
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.

Benoit

unread,
Jan 12, 2022, 9:11:56 PM1/12/22
to Metamath
I think you were thinking of Alexander's mathbox, not mine !

The statement that looks more natural is  |-  A. n e. O ( ( ; 1 0 ^ ; 2 7 ) < n -> n e. G ) (at Step 127 of your proof), and it looks also more directly usable by ~tgoldbach in Alexander's mathbox.

Benoît

Alexander van der Vekens

unread,
Jan 13, 2022, 11:14:41 AM1/13/22
to Metamath
According to our rules, I cannot use ~tgoldbachgt in my Mathbox as long as it is in Thierry`s mathbox! Maybe we can move the whole material from both mathboxes to main set.mm? One difficulty would be, however, that I intensivly use the classes Even and Odd (defined in my mathbox), which were not allowed to be moved to main set.mm yet (see github issue #1682).

Jim Kingdon

unread,
Jan 13, 2022, 3:01:51 PM1/13/22
to meta...@googlegroups.com

I've tried to write up the situation about Even and Odd at https://github.com/metamath/set.mm/issues/2433 . Hopefully it is helpful for me to summarize what was a rather long thread the last time this came up.

Hopefully we can find a solution - it would be kind of silly if figuring out how to say "x is odd" prevents us from getting things out of mathboxes which we otherwise would like to.

Thierry Arnoux

unread,
Jan 13, 2022, 11:02:53 PM1/13/22
to meta...@googlegroups.com, Jim Kingdon

Indeed this is a good opportunity to raise (again) the question about the definition of odd integers.

I agree with Norm that` 2 || N ` is just as long as ` N e. Even `, and therefore will not bring any database size improvement. Since it also implies ` 2 e. ZZ `, I don't see worth in defining `Even`.

For `Odd` this does not hold, one cannot just replace it with ` -. 2 || N ` but also has to add ` N e. ZZ ` to recover a definition of `Odd`.

To circumvent this, I have been using essential hypotheses in the form of ` O = { z e. ZZ | -. 2 || z } `, like in ~ hgt749d and ~ eulerpart.

This allows me to use the local `O` in the proof just like if it were a definition. We could also use this trick in main without defining a new symbol.


Anyway, I'd also like to point out that technically, nothing prevents Alexander (sorry for the mix-up in my previous mail) to use theorems from my Mathbox; this rule is nowhere enforced. Maybe a short comment that this goes against the usage and why we chose to make an exception would also work!

BR,
_
Thierry

Alexander van der Vekens

unread,
Jan 14, 2022, 12:05:11 AM1/14/22
to Metamath
On Friday, January 14, 2022 at 5:02:53 AM UTC+1 Thierry Arnoux wrote:
...

Anyway, I'd also like to point out that technically, nothing prevents Alexander (sorry for the mix-up in my previous mail) to use theorems from my Mathbox; this rule is nowhere enforced. Maybe a short comment that this goes against the usage and why we chose to make an exception would also work!


Actually, it is enforced not to use theorems of other's mathboxes: on running "verify markup", there will be warning, for example:

?Warning: The proof of "tgoldbachgtX" in the mathbox for Alexander van der
    Vekens references "tgoldbachgt" in the mathbox for Thierry Arnoux.

If it is not accepted to have a dedicated symbol "Odd" (and if we have such a symbol, we also should have a symbol "Even" for symmetry reasons, although it would not really be needed), I already though of using Thierry's local `O`, but let's discuss this further in the github issue #2433 opend by Jim.

Benoit

unread,
Jan 14, 2022, 7:51:53 AM1/14/22
to Metamath
I think we can separate both issues (the question of symbols for Even/Odd being discussed on github, and the question of mutual mathbox uses).  Probably the best option is: if mathbox A uses the theorem xxx proved in mathbox B, then add to mathbox A the axiom ax-xxx with exactly the same statement as xxx and put a comment like "Duplicate of ~ xxx."

As for moving to Main, I think it is premature because both mathboxes show conditional proofs (actually, "very conditional", in the sense that the intermediate steps posited as axioms are not anecdotal, it seems, but correct me if I'm wrong).  Conditional proofs are fine for works in progress, but Main is not for works in progress, and moving conditional proofs to Main could be seen from the outside as bragging about Metamath being able to prove this and that.  Again, there may be exceptions and I haven't looked at the present case enough.

A more general remark: we should strive to maintain the high review standards of Main, and I fear sometimes that the following may happen: when theorems are introduced in a mathbox, reviewer A thinks "it's in a mathbox, so a cursory review suffices and if/when it is moved to Main, a thorough review will be done anyway", and later when that part is moved to Main, reviewer B thinks "it's only a move of something already in set.mm so it has been already reviewed, so a cursory review suffices".  I'm not worried about contributions from long-time contributors Thierry and Alexander (although everyone may make mistakes), but more about future contributions.

Benoît

Alexander van der Vekens

unread,
Jan 15, 2022, 1:38:13 AM1/15/22
to Metamath
I want to point to a former discussion https://groups.google.com/g/metamath/c/mnkBQV1_cXc (starting with an impressive essay written by Norm), in which the question what and how to move definitions/theorems to main set.mm is discussed. Especially my proposal to introduce an additional layer betwen main set.mm and the mathboxes (see https://groups.google.com/g/metamath/c/mnkBQV1_cXc/m/A5OEsTk7AQAJ) could be helpful here: Such an "incubator layer" could be a place for definitions/theorems which are not experimental anymore, but not mature enough to be moved to main set.mm.  This could also support the review process described by Benoît.  

Alternatively, we could create a "Mathbox for Christian Goldbach" where we could place Thierry's and my material about Goldbach's conjecture.

Alexander van der Vekens

unread,
Jan 15, 2022, 4:12:04 AM1/15/22
to Metamath
On Friday, January 14, 2022 at 1:51:53 PM UTC+1 Benoit wrote:
I think we can separate both issues (the question of symbols for Even/Odd being discussed on github, and the question of mutual mathbox uses).  Probably the best option is: if mathbox A uses the theorem xxx proved in mathbox B, then add to mathbox A the axiom ax-xxx with exactly the same statement as xxx and put a comment like "Duplicate of ~ xxx."

This is a good idea (for an intermediate solution), therefore I have adapted my mathbox as Benoît proposed in my current PR https://github.com/metamath/set.mm/pull/2434.
Reply all
Reply to author
Forward
0 new messages