All: Metamath-lamp proof assistant version 11 has now been released! This is a proof assistant for Metamath that can run directly on your web browser, including one on your smartphone. You can use it here: https://expln.github.io/lamp/latest/index.html
Major additions in version 11: * Added an "explorer tab" and dynamic tabs for existing proofs, enabling users to examine the current context at any time. * Works well on smartphones (e.g., supports "long-click" or "long-tap") * More unified UI - all edits by default use a "long-click". * Supports identifying one provable statement as the "goal statement" and treats it specially, making the UI easier to use. * Visualization can be enabled or disabled per justification * More control over which fields are displayed during editing Documentation is available at: https://lamp-guide.metamath.org/ Videos showing how to use Metamath-lamp version 11: "Introduction to Metamath-lamp, part 1" - https://youtu.be/b-RfoUuQpAQ "Introduction to Metamath-lamp, part 2" - https://youtu.be/WOp2xQ8mEE4 "Introduction to Metamath-lamp, part 3" - https://youtu.be/Aqp3jAM2b60 I'm posting this on behalf of @expln, who actually wrote the tool; I'm just trying to help potential users by writing some documentation & making videos. <https://github.com/expln/metamath-lamp/issues/120> --- David A. Wheeler -- 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/CDE8F7A0-0E49-4BE0-AD13-47E8064F67CD%40dwheeler.com.
