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:
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:
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
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 `
--
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/ad7e9314-b275-40bf-a858-a1bb8b6fda85n%40googlegroups.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.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4af279b8-54c9-4e70-9847-9907c76458e7n%40googlegroups.com.
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
...
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!
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."