Metamath-lamp version 11 has been released!

29 views
Skip to first unread message

David A. Wheeler

unread,
Jun 26, 2023, 5:34:10 PM6/26/23
to Metamath Mailing List
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

Reply all
Reply to author
Forward
0 new messages