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 On Thursday, January 13, 2022 at 3:01:14 AM UTC+1 Thierry Arnoux wrote: > 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, 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 > > > 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, 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 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 >>> <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 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! >>> >>> 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/1dda7d78-4e34-4b2e-8449-ffecc58fedbdn%40googlegroups.com.
