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 from the technical point of view:
This is a pretty new tool, I tested it on only simple proofs and use cases. So far it worked well for me. I do my best to cover complex functions with unit and integration tests. But without "testing in the field" I cannot assure that there are no bugs. And this is not a java application when if it works on developer's computer then most probably it will work on many other computers. It is JavaScript code running in a browser and risks of something may go wrong for other users is higher than in the case of a typical java application, for example. metamath-lamp runs completely in a browser so I will not know how often and how successfully it is used by others. 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. - Igor On Sunday, May 28, 2023 at 11:19:01 AM UTC+2 Alexander van der Vekens wrote: > 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 > Applet (does it actually work somewhere/somehow?) very soon. Maybe a > restriction of the scope (for beginners) could help: if only propositional > or predicate calculus (or ZF set theory) is used (this is a great > functionality of methamath-lamp to restrict the amount of set.mm to be > loaded and used. "Stop at exists2" would only load definitions and theorems > for propositional or predicate calculus, "Stop at hsmex3" for ZF set > theory), metamath-lamp may be fast and intuitive enough for a beginner. > > -- 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/8f557136-b1cc-4b7f-add7-1f0ed4275280n%40googlegroups.com.
