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 On 13/01/2022 03:44, Benoit wrote:
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 <http://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 <http://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 On Wednesday, January 12, 2022 at 7:40:55 PM UTC+1 Glauco wrote: Great job, Thierry. Il giorno mercoledì 12 gennaio 2022 alle 04:48:37 UTC+1 Thierry Arnoux ha scritto: 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 <https://github.com/tirix/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 <http://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 <https://github.com/metamath/metamath-exe/issues/31#issuecomment-1006328448> in a recent comment ;) ). For now, it only serves set.mm <http://set.mm> pages. It would not be very hard to extend it to e.g. iset.mm <http://iset.mm>. There are only two renderers implemented until now: * the unformatted ASCII source file, which uses "mpeascii <http://metamath.tirix.org:3030/mpeascii/tgoldbachgt.html>" in the path, * the so-called "structured typesetting" (STS), with "mpests <http://metamath.tirix.org:3030/mpests/tgoldbachgt.html>" 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 <http://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: * Jannik's shorter proof of the irrationality of the square root of 2 <http://metamath.tirix.org:3030/mpests/sqr2irrlem.html>, * Scott's full-eta axiom for the surreal numbers <http://metamath.tirix.org:3030/mpests/noeta.html> (and more), * Alexander's shorter version of Huneke's proof <http://metamath.tirix.org:3030/mpests/frgr2wwlk1.html> , and sum of degrees of a finite pseudograph <http://metamath.tirix.org:3030/mpests/finsumvtxdg2size.html>, * Glauco's inferior limit of a countable set of sigma measurable function <http://metamath.tirix.org:3030/mpests/smfliminf.html>, * my last step of the Ternary Goldbach Conjecture <http://metamath.tirix.org:3030/mpests/tgoldbachgt.html> 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 <http://iset.mm>! 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ad7e9314-b275-40bf-a858-a1bb8b6fda85n%40googlegroups.com <https://groups.google.com/d/msgid/metamath/ad7e9314-b275-40bf-a858-a1bb8b6fda85n%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2cb3c08c-0809-c3ea-19ff-af71f5482369%40gmx.net.
