Re: [Metamath] Future website directions

On Thu, Mar 2, 2023 at 5:37 PM David A. Wheeler wrote: > > > > On Thu, Mar 2, 2023 at 12:53 PM David A. Wheeler > wrote: > > 2. The text just runs off to the right, instead of going over multiple > lines, making long ones unreadable. That's important but easy for the > non-MathML case (just a

Re: [Metamath] Future website directions

> On Thu, Mar 2, 2023 at 12:53 PM David A. Wheeler > wrote: > 2. The text just runs off to the right, instead of going over multiple lines, > making long ones unreadable. That's important but easy for the non-MathML > case (just a little CSS), though I don't know how hard that is for >

Re: [Metamath] Future website directions

On Thu, Mar 2, 2023 at 12:53 PM David A. Wheeler wrote: > 2. The text just runs off to the right, instead of going over multiple > lines, making long ones unreadable. That's important but easy for the > non-MathML case (just a little CSS), though I don't know how hard that is > for

Re: [Metamath] Future website directions

Hi David,  At least, there was one that let you expand/contract proof steps, which one was that? The viewer you're talking about is probably this one: http://metamath.tirix.org/geoisum1.html There are two things in there: First, this is also MathML, but this time generated not using

Re: [Metamath] Future website directions

> On Feb 27, 2023, at 5:27 PM, Thierry Arnoux wrote: > > And since we're there, I'd also like to recall this other live site: > > http://metamath.tirix.org:3030/mpests/toc > > All pages are rendered dynamically, there are 3 modes: > > - ASCII -

Re: [Metamath] Future website directions

And since we're there, I'd also like to recall this other live site: http://metamath.tirix.org:3030/mpests/toc All pages are rendered dynamically, there are 3 modes: - ASCII - Unicode -

Re: [Metamath] Future website directions

> On Feb 26, 2023, at 11:04 PM, Mario Carneiro wrote: > > FYI I did a fairly comprehensive HTML modernization in mm-web-rs > [https://github.com/digama0/mm-web-rs/blob/master/src/render.rs] (which is > basically a clone of the metamath-exe theorem page generator), which among > other

Re: [Metamath] Future website directions

FYI I did a fairly comprehensive HTML modernization in mm-web-rs [ https://github.com/digama0/mm-web-rs/blob/master/src/render.rs] (which is basically a clone of the metamath-exe theorem page generator), which among other things lowercased all the tags and made it pass the w3c validator again

Re: [Metamath] Future website directions

I completely agree, a page on AI/ML would be great. The pages could do with a refresh anyway, many places suggest contacting Norm. Norm used an HTML 1.0 convention of using uppercase tags. I suggest that new text use lowercase tags as a style choice It doesn't matter technically, but it is the

Re: [Metamath] Future website directions

A page with short descriptions of papers and projects using Metamath for AI would be great to put on the website. I think it would be good publicity for both metamath and the AI systems, and maybe we can solicit the paper authors to write the descriptions and provide related links as well. On

Re: [Metamath] Future website directions

Re the subject of LLMs being trained on metamath this new model called LLama from facebook is interesting. It seems to be smaller than other systems and it looks like they're already training on metamath. https://ai.facebook.com/blog/large-language-model-llama-meta-ai/ It links to this page

Re: [Metamath] Future website directions

> On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler > wrote: > My first choice when building a website, where it's easily achieved, is > static rendering (statically-generated pages) where the most important data > is visible without client-side JavaScript. Those are easily understood, >

Re: [Metamath] Future website directions

That's very much on my roadmap, but I had to start with .mm because I don't believe the code for generating .mmp files exists on the JavaScript platform yet. (Glauco's Yamma doesn't have it yet, and Igor's proof assistant doesn't use them or save any intermediate format I'm aware of). The

Re: [Metamath] Future website directions

On Sun, Feb 19, 2023 at 1:05 PM Mario Carneiro wrote: > I don't see those as competing goals at all. They play different roles: > for browsing you would ideally have some server supplying only the required > information to render a specific proof, and for a proof assistant (and to > some extent

Re: [Metamath] Future website directions

On Sun, Feb 19, 2023 at 2:19 PM David A. Wheeler wrote: > > While yes I agree that this would be much better done with > metamath-knife than metamath-exe, I don't think there is a major concern > here, or at least we can mostly mitigate the issues since this flow is > extremely light on input

[Metamath] Future website directions

FYI: Our discussion topic seems to have broadened to discussing potential future directions for the website, so I've changed the subject line to "Future website directions". Its subject line was previously: "Re: [Metamath] Idea: Release ".txt" proofs for set.mm databases ("mpetxt") for AI/ML