Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

> Therefore there is a risk that official Metamath site suggests a tool which performs not so good as it has to and nobody knows that. I don't think this is a major concern, as long as we manage expectations on the landing page. Metamath and all associated tools come with no warranty, after all.

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

I want to add few more things to consider before suggesting metamath-lamp as a proof assistant to start with in the first place. Not that I don't want a tool I am developing to be present on the front page of the official Metamath site :) But I think I have to mention what may be not so obvious

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

Hi Igor, hi David, I think the current status of metamath-lamp is already very good, but not good enough for a beginner. So there is room for some improvements (especially regarding documentation, as indicated by David). In any case, it is a good candidate to replace the Metamath Solitaire

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

*>>> you have to know some basic metamath theorems in advance* My goal is exactly opposite :) That's why I designed the interface this way when justifications are not shown by default and users see only statements and if they are proved or not. Apparently this goal is not fully achieved so far

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

> On Friday, May 26, 2023 at 11:10:02 PM UTC+2 David A. Wheeler wrote: > > Ask and ye shall receive!! As of this morning the first draft of the > metamath-lamp guide is available here: > https://github.com/expln/metamath-lamp/blob/master/docs/guide.md > On May 27, 2023, at 10:17 AM,

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

OK I tried it again using On Friday, May 26, 2023 at 11:10:02 PM UTC+2 David A. Wheeler wrote: Ask and ye shall receive!! As of this morning the first draft of the metamath-lamp guide is available here: https://github.com/expln/metamath-lamp/blob/master/docs/guide.md I wanted to proof ( 5

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

> On May 26, 2023, at 4:19 PM, 'Alexander van der Vekens' via Metamath > wrote: > > I just had a look at metamath-lamp itself and at the video. It is actually > very impressive, but, to be honest, I have no idea how to use it. There is an > urgent need for instructions, a user guide, a

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

I just had a look at metamath-lamp itself and at the video. It is actually very impressive, but, to be honest, I have no idea how to use it. There is an urgent need for instructions, a user guide, a tutorial, etc. before it can be recommened for beginners... -- You received this message

Re: [Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

Hi David, Good idea! I think we should also list Yamma: https://marketplace.visualstudio.com/items?itemName=glacode.yamma I've been using it recently to write my latest proofs, and it is quite functional. BR, _ Thierry On 24/05/2023 03:24, David A. Wheeler wrote: I've been

[Metamath] metamath-lamp is impressive, check it out, and let's eventually modify the Metamath front page to mention it (at least)

I've been experimenting with the proof assistant metamath-lamp, including abusing poor Igor with a variety of suggestions :-). In short: I'm quite impressed with metamath-lamp. Of the functions that I routinely *use* in mmj2, the only one that I really miss is mmj2's automation routines. I'm sure