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).
On Thursday, January 13, 2022 at 3:11:56 AM UTC+1 Benoit wrote: > 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/4af279b8-54c9-4e70-9847-9907c76458e7n%40googlegroups.com.
